/* ************************************************************************
 *            MCMAS -- Model Checker for Multi-Agent Systems
 *
 *     Copyright (C) 2007, 2008
 *     Hongyang Qu and Franco Raimondi and Alessio Lomuscio
 *     This program is free software; you can redistribute it and/or modify
 *     it under the terms of the GNU General Public License as published by
 *     the Free Software Foundation; either version 2 of the License, or
 *     (at your option) any later version.
 *     This program is distributed in the hope that it will be useful,
 *     but WITHOUT ANY WARRANTY; without even the implied warranty of
 *     MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *     GNU General Public License for more details.
 *
 *   You should have received a copy of the GNU General Public License
 *   along with this program; if not, write to the Free Software
 *   Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 *
 **************************************************************************/

#include "main.hh"

/*
 #define REORDER_OFF 0
 #define FORCED_REORDER 0
 #define AUTO_REORDER 1
 */

void MCMAS_Cudd_AutodynEnable(DdManager * unique, Cudd_ReorderingType method)
{
    printf("MCMAS ENABLE CALLED...\n");
#if AUTO_REORDER
    printf("CUDD ENABLE CALLED...\n");
    Cudd_AutodynEnable(unique, method);
#endif

    return;
}

using namespace std;

int main(int argc, char* argv[])
{
    time_t t0 = time(0);
    no_kbar = false;

    setup(argc, argv);

#if REORDER_OFF
    printf("REORDER_OFF\n");
#elif FORCED_REORDER
    printf("FORCED_REORDER\n");
#else
    printf("AUTO_REORDER\n");
#endif

    simulate();

    // REORDERING OF VARIABLES:
    Cudd_ReorderingType REORDERING = CUDD_REORDER_GROUP_SIFT_CONV;
    if (options["optimization"] == 0 || options["optimization"] == 2)
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), REORDERING);

    if (options["experiment"] == 0)
    {
        experiment_0();
    }
    else
    { // ---------------------- experiment  ------------------------
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), REORDERING);
        if (options["initialfirst"] == 1)
        {
            if (options["quiet"] == 0 || options["simulation"] == 0)
            {
                cout << "Building OBDD for initial states...";
                cout.flush();
            }
            //options["debug"] = 1;
            //scount = 0;*/
            in_st = (options["flatexpression"] < 2) ? is_istates->encode_bdd(
                    bddOne) : is_istates->encode_bdd_flat(bddOne);
            in_st = append_variable_BDDs(in_st);
            //options["debug"] = 0;
            //MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), REORDERING);
            if (options["verbosity"] > 3)
                cout << "Done." << endl;
        }
        if (options["quiet"] == 0 || options["simulation"] == 0)
        {
            cout << "Building partial transition relation..." << endl;
        }
        for (unsigned int i = 0; i < agents->size(); i++)
        {
            if (options["verbosity"] > 3)
            {
                if (i == 0)
                    cout << endl;
                cout << "      Processing " << (*agents)[i]->get_name()
                        << ": protocol... ";
                //cout.flush();
            }
            time_t tmpt0 = time(0);
            (*vprot)[i] = (*agents)[i]->encode_protocol();
            if (options["verbosity"] > 3)
            {
                cout << "done, evolution...";
                //cout.flush();
            }
            (*vevol)[i] = (*agents)[i]->encode_evolution();
            if (options["verbosity"] > 3)
            {
                cout << "done, local transition relation...";
                //cout.flush();
            }
            (*vRT)[i] = (*vprot)[i] * (*vevol)[i];
            time_t tmpt1 = time(0);
            if (options["verbosity"] > 3)
            {
                cout << "done. " << difftime(tmpt1, tmpt0) << " seconds"
                        << endl;
            }
            //MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
        }
        if (options["verbosity"] > 3)
            cout << "Done" << endl;
        if (options["initialfirst"] == 0)
        {
            if (options["quiet"] == 0 || options["simulation"] == 0)
            {
                cout << "Building OBDD for initial states..." << endl;
            }
            in_st = (options["flatexpression"] < 2) ? is_istates->encode_bdd(
                    bddOne) : is_istates->encode_bdd_flat(bddOne);
            in_st = append_variable_BDDs(in_st);
            if (options["verbosity"] > 3)
                cout << "Done." << endl;
        }
        //REORDERING = CUDD_REORDER_WINDOW4_CONV;
        //MCMAS_Cudd_AutodynEnable(bddmgr->getManager(),REORDERING);
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);

        if (options["quiet"] == 0 || options["simulation"] == 0)
        {
            cout << "Building reachable state space..." << endl;
        }
        if (options["experiment"] == 1)
        {
            experiment_1();
            check_formulae();
        }
        else if (options["experiment"] == 2)
        {
            experiment_2();
            check_formulae();
        }
        else if (options["experiment"] == 3)
        {
            experiment_3();
            check_formulae();
        }
        else if (options["experiment"] == 4)
        {
            experiment_4();
        }
        else if (options["experiment"] == 5)
        {
            if (options["bmcslave"] == 1)
            {
                experiment_5_Slave();
            }
            else
            {
                experiment_5_Master();
            }
        }
        else if (options["experiment"] == 6)
        {
            experiment_6();
        }
        else
        {
            experiment_1();
            check_formulae();
        }
    }
    //MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);

    int verb = options["verbosity"];
    //options["verbosity"] = 0;
    if (options["verbosity"] > 6)
    {
        cout << "Reachable states: " << endl;
        reach.print(2, 2);
    }
    options["verbosity"] = verb;

    if (options["verbosity"] > 4)
        cout << "Done." << endl;

    if (options["quiet"] == 0)
        cout << "done, " << is_formulae->size()
                << " formulae successfully read and checked" << endl;

    time_t t1 = time(0);
    //if(options["verbosity"] > 4) {
    cout << "execution time = " << difftime(t1, t0) << endl;
    double reachablestates = reach.CountMinterm(v->count());
    cout << "number of reachable states = " << reachablestates << endl;
    unsigned long memoryinuse = bddmgr->ReadMemoryInUse();
    cout << "BDD memory in use = " << memoryinuse << endl;
    //}
    if (options["bdd_stats"] == 1)
    {
        bddmgr->info();
    }

    //    Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
    //
    //    DdNode* f = (reach.getNode());
    //    DdNode** bdd_trees = (DdNode**)malloc(sizeof(DdNode*)); //we have only one BDD tree
    //    bdd_trees[0] = f;
    //    FILE* fp = fopen("out.dot", "w");
    //    Cudd_DumpDot(bddmgr->getManager(), 1, bdd_trees, NULL, NULL, fp);
    //    fclose(fp);
}

void setup(int argc, char* argv[])
{
    is_agents = new map<string, basic_agent *> ;
    agents = new vector<basic_agent *> ;
    is_evaluation = new map<string, bool_expression *> ;
    is_groups = new map<string, set<string> > ;
    is_formulae = new vector<modal_formula> ;
    is_fairness = new vector<fairness_expression *> ;

    atomic_k_bar_formula = NULL;

    options["verbosity"] = 0;
    options["pnode_info"] = 0;
    options["bdd_stats"] = 0;
    options["uniform"] = 0;
    options["globalcheck"] = 0;
    options["debug"] = 0;
    options["cex"] = 0;
    options["simulation"] = 0;
    options["source"] = 0;
    options["syncheck"] = 0;
    options["nobanner"] = 0;
    options["quiet"] = 0;
    options["experiment"] = 1;
    options["initialfirst"] = 0;
    options["optimization"] = 0;
    options["symmetry"] = 0;
    options["bddcache"] = 3;
    options["flatexpression"] = 0;
    options["lazyGCK"] = 0;
    options["bmcslave"] = 0;

    static const std::string verb("-v");
    static const std::string binfo("-bdd_stats");
    static const std::string uniform("-u");
    static const std::string globalcheck("-g");
    static const std::string help("-h");
    static const std::string help2("--help");
    static const std::string debug("-d");
    static const std::string cex("-c");
    static const std::string simulation("-s");
    static const std::string source("-src");
    static const std::string syncheck("-gsc");
    static const std::string nobanner("-nb");
    static const std::string quiet("-q");
    static const std::string experiment("-e");
    static const std::string bddcache("-bc");
    static const std::string initialfirst("-if");
    static const std::string optimization("-op");
    static const std::string cexoutdir("-cex_prefix");
    static const std::string symmetry("-symmetry");
    static const std::string flatexpression("-fe");
    static const std::string lazyGCK("-lgck");
    static const std::string initbddfileop("-init_bdd_file");
    static const std::string bmcslave("-bmc_slave");
    static const std::string oneshot("-one_shot");

    std::string filename;

    string s;

    mcmas_driver driver;

    calReachRT = true;

    if (argc < 2)
    {
        print_help();
        exit(1);
    }

    cex_prefix = "";
    initbddfile = "";
    for (int i = 1; i < argc - 1; ++i)
    {
        if (binfo == argv[i])
        {
            options["bdd_stats"] = 1;
            //} else if (uniform == argv[i]) {
            ///options["uniform"] = 1;
            //} else if (debug == argv[i]) {
            //options["debug"] = 1;
        }
        else if (cex == argv[i])
        {
            options["cex"] = 1;
        }
        else if (verb == argv[i])
        {
            string s;
            s = argv[++i]; // consume the argument
            options["verbosity"] = atoi(s.c_str());
        }
        else if (globalcheck == argv[i])
        {
            options["globalcheck"] = 1;
        }
        else if ((help == argv[i]) || (help2 == argv[i]))
        {
            print_help();
            exit(1);
        }
        else if (simulation == argv[i])
        {
            options["simulation"] = 1;
            //} else if (source == argv[i]) {
            //options["source"] = 1;
            //} else if (lazyGCK == argv[i]) {
            //options["lazyGCK"] = 1;
            //} else if (syncheck == argv[i]) {
            //options["syncheck"] = 1;
        }
        else if (nobanner == argv[i])
        {
            options["nobanner"] = 1;
        }
        else if (quiet == argv[i])
        {
            options["quiet"] = 1;
        }
        else if (experiment == argv[i])
        {
            string s;
            s = argv[++i]; // consume the argument
            options["experiment"] = atoi(s.c_str());
            //} else if (bddcache == argv[i]) {
            //string s;
            //s = argv[++i]; // consume the argument
            //options["bddcache"] = atoi(s.c_str());
        }
        else if (initialfirst == argv[i])
        {
            options["initialfirst"] = 1;
            //} else if (optimization == argv[i]) {
            //string s;
            //s = argv[++i]; // consume the argument
            //options["optimization"] = atoi(s.c_str());
        }
        else if (cexoutdir == argv[i])
        {
            string s;
            s = argv[++i]; // consume the argument
            cex_prefix = s;
            //} else if (symmetry == argv[i]) {
            //string s;
            //s = argv[++i]; // consume the argument
            //options["symmetry"] = atoi(s.c_str());
        }
        else if (flatexpression == argv[i])
        {
            string s;
            s = argv[++i]; // consume the argument
            options["flatexpression"] = atoi(s.c_str());
        }
        else if (initbddfileop == argv[i])
        {
            string s;
            s = argv[++i];
            initbddfile = s;
        }
        else if (bmcslave == argv[i])
        {
            options["bmcslave"] = 1;
        }
        else if (oneshot == argv[i])
        {
            string s;
            s = argv[++i];
            one_shot_depth = atoi(s.c_str());
        }
        else
        {
            // whether to do anything about unexpected
            // arguments is a matter of taste (see below)
            cout << NAME << " invalid option: " << argv[i] << endl;
            print_help();
            exit(1);
        }
    }

    if (options["nobanner"] == 0 && options["quiet"] == 0)
        print_banner();

    if ((help == argv[argc - 1]) || (help2 == argv[argc - 1]))
    {
        print_help();
        exit(1);
    }

    filename = argv[argc - 1];

    if (options["debug"] == 1)
    {
        cout << "DEBUG: filename" << endl;
        cout << "    " << filename << endl;
        cout << "DEBUG: end filename" << endl;
    }

    driver.parse(filename);
    if (!driver.syntax_error)
    {
        if (options["quiet"] == 0 || options["simulation"] == 0)
            cout << filename << " has been parsed successfully." << endl;
        if (options["source"] == 1)
        {
            print_ispl_code();
            exit(0);
        }
        if (options["quiet"] == 0 || options["simulation"] == 0)
            cout << "Global syntax checking..." << endl;
        if (!global_consistency_check())
        {
            cout << filename << " has error(s)." << endl;
            exit(-1);
        }
        if (options["quiet"] == 0)
            cout << "Done" << endl;
        if (options["syncheck"] == 1)
            exit(0);
    }
    else
    {
        cout << filename << " has syntax error(s)." << endl;
        exit(-1);
    }

    if (options["experiment"] == 4 || options["experiment"] == 2
            || options["experiment"] == 5 || options["experiment"] == 6)
    {
        // BMC

        bmc_formulae = new vector<modal_formula_p_pair> ;
        bmc_false_formulae = new vector<modal_formula_p_pair> ;
        int error = 0;

        for (unsigned int i = 0; i < is_formulae->size(); i++)
        {
            modal_formula *actl = &(*is_formulae)[i];

            modal_formula *actl_pushed = actl->push_negations(0);
        
            if (actl_pushed->is_ECTLK_BMC())
            {
                bmc_formulae->push_back(modal_formula_p_pair(actl, actl_pushed));
                continue;
            }

            modal_formula *actl_pushed_negated = new modal_formula(3,
                    actl_pushed);
            modal_formula *ectl = actl_pushed_negated->push_negations(0);

            if (!actl->is_ACTLK_BMC() || !ectl->is_ECTLK_BMC())
            {
                if (!error)
                {
                    cout
                            << "When using BMC, all formulae should be in ACTLK. The following formulae are *not* ACTLK:"
                            << endl;
                }
                error = 1;
                cout << "    * " << actl->to_string() << endl;
            }
            else
                bmc_formulae->push_back(modal_formula_p_pair(actl, ectl));
        }

//        if ((options["experiment"] == 5) && (options["bmcslave"] == 1) &&
//        		(is_formulae->size() == 1) && ((*is_formulae)[0].get_op() == 13))
//        {
//        	cout << "BMC SLAVE WITH EX" << endl;
//        }

        if (error)
        {
            cout
                    << "Please correct these formulae. Verification will not continue."
                    << endl;

            exit(-1);
        }
    }

    if (options["experiment"] == 5 && (options["bmcslave"] == 0))
    {
        if (bmc_formulae->size() != 1)
        {
            cout << "Distributed model checking only supports a single formulae at a time.";
            cout << "Please correct this model. Verification will not continue";
            cout.flush();
            exit(-1);
        }

        bool atomic_k_bar = bmc_formulae->at(0).second->atomic_k_bar(&atomic_k_bar_formula);

        if (!atomic_k_bar)
        {
            cout << "Distributed model checking only supports invariant formulae with atomic knowledge definitions";
            cout << "Please correct this model. Verification will not continue";
            cout.flush();
            exit(-1);
        }

        cout << (atomic_k_bar ? "True" : "False") << "," << (atomic_k_bar ? atomic_k_bar_formula->to_string() : "NULL") << endl;

    }

    /*if (options["debug"] == 1) {
     cout << "DEBUG: begin ISPL code" << endl;
     print_ispl_code();
     cout << "DEBUG: end ISPL code" << endl;
     }*/

    if (options["verbosity"] > 2)
    {
        cout << "Starting OBDD manager...";
    }

    if (options["experiment"] == 2 || options["experiment"] == 4
            || options["experiment"] == 5 || options["experiment"] == 6)
    {
        bddmgr = new Cudd(0, 0, 0, 0, 0);
    }
    else
    {
        bddmgr = new (Cudd);
    }

    if (options["experiment"] == 2 || options["experiment"] == 4
            || options["experiment"] == 5 || options["experiment"] == 6)
    {
#if !AUTO_REORDER
        cout << "Disabling cache" << endl;
        Cudd_AutodynDisable(bddmgr->getManager());
#endif
    }

    bddOne = new BDD(bddmgr->bddOne());
    reach = bddmgr->bddZero();

    if (options["verbosity"] > 2)
    {
        cout << "Done" << endl;
    }

    if (options["simulation"] == 0 || options["quiet"] == 0)
        cout << "Encoding BDD parameters..." << endl;

    // Calculate the number of BDD variables for states and actions
    int states_count = 0;
    int actions_count = 0;
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        states_count += (*agents)[i]->state_BDD_length();
        actions_count += (*agents)[i]->actions_BDD_length();
    }

    if (options["verbosity"] > 3)
    {
        cout << endl << "  Building BDDs variables...";
    }

    v = new BDDvector(states_count, bddmgr); // Local states
    addv = new ADDvector(states_count, bddmgr);
    pv = new BDDvector(states_count, bddmgr); // "Next" local states
    addpv = new ADDvector(states_count, bddmgr);
    a = new BDDvector(actions_count, bddmgr); // Actions

    // Allocate BDD variables to states and actions
    for (int i = 0; i < states_count; i++)
    {
        (*v)[i] = bddmgr->bddVar(i);
        (*pv)[i] = bddmgr->bddVar(states_count + i);
        (*addv)[i] = bddmgr->addVar(i);
        (*addpv)[i] = bddmgr->addVar(states_count + i);
    }
    for (int i = 0; i < actions_count; i++)
        (*a)[i] = bddmgr->bddVar(states_count * 2 + i);

    if (options["verbosity"] > 3)
    {
        cout << "Done: " << v->count() << " for local states, " << a->count()
                << " for actions." << endl;
    }

    // Calculate the position of every variable and every set of actions
    int k1 = 0;
    int k2 = 0;
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        k1 = (*agents)[i]->allocate_BDD_2_variables(k1);
        k2 = (*agents)[i]->allocate_BDD_2_actions(k2);
    }

    if (options["debug"] == 1)
    {
        cout << endl << "BDD index and encoding of all values of all variables"
                << endl;
        for (unsigned int i = 0; i < agents->size(); i++)
        {
            cout << (*agents)[i]->get_name() << ":" << endl;
            (*agents)[i]->print_variable_BDD_encoding();
            cout << endl;
        }
    }

    obsvars_bdd_length = (*agents)[0]->obsvars_BDD_length();
    envars_bdd_length = (*agents)[0]->get_var_index_end();

    // Encode initial states
    in_st = bddmgr->bddOne();
}

void simulate(void)
{
    if (options["experiment"] >= 1 || options["simulation"] == 1)
    {
        vprot = new BDDvector(agents->size(), bddmgr);
        vevol = new BDDvector(agents->size(), bddmgr);
        vRT = new BDDvector(agents->size(), bddmgr);
    }
    if (options["simulation"] == 1)
    {
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(),
                CUDD_REORDER_GROUP_SIFT_CONV);
        in_st
                = (options["flatexpression"] < 2) ? is_istates->encode_bdd(
                        bddOne) : is_istates->encode_bdd_flat(bddOne);
        in_st = append_variable_BDDs(in_st);
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(),
                CUDD_REORDER_GROUP_SIFT_CONV);
        if (in_st == bddmgr->bddZero())
        {
            cout << "No initial state. Check your model!" << endl;
            exit(0);
        }
        for (unsigned int i = 0; i < agents->size(); i++)
        {
            (*vprot)[i] = (*agents)[i]->encode_protocol();
            (*vevol)[i] = (*agents)[i]->encode_evolution();
            (*vRT)[i] = (*vprot)[i] * (*vevol)[i];
        }
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
        BDDvector inistates(MAXINISTATES, bddmgr);
        int count = 0;
        BDD is = in_st;
        map<string, int> statehash;
        while (count < MAXINISTATES && is != bddmgr->bddZero())
        {
            inistates[count] = is.PickOneMinterm(*v);
            is = is - inistates[count];
            if (is_valid_state(inistates[count], *v))
            {
                string state = state_to_str(inistates[count], *v);
                if (!find_same_state(&statehash, state))
                {
                    statehash[state] = 1;
                    count++;
                }
            }
        }
        if (options["quiet"] == 0)
        {
            if (count == MAXINISTATES && is != bddmgr->bddZero())
                cout
                        << "There are too many initial states. Please specify more initial values."
                        << endl;
            while (true)
            {
                BDDvector stack(MAXSTACKDEPTH, bddmgr);
                int sp = 0;
                cout << endl << "--------- Initial state ---------" << endl;
                int isindex = 0;
                print_state(inistates[isindex], *v);
                cout << "----------------------------" << endl;
                if (count > 1)
                {
                    bool choose = false;
                    string c;
                    while (!choose)
                    {
                        if (isindex == 0)
                            cout
                                    << "Is this the initial state? [Y(es), N(ext), E(xit)]: ";
                        else if (isindex == count - 1)
                            cout
                                    << "Is this the initial state? [Y(es), P(revious), E(xit)]: ";
                        else
                            cout
                                    << "Is this the initial state? [Y(es), N(ext), P(revious), E(xit)]: ";
                        cin >> c;
                        transform(c.begin(), c.end(), c.begin(),
                                (int(*)(int)) tolower);
                        if (c == "y" || c == "yes")
                        {
                            choose = true;
                            break;
                        }
                        else if ((isindex < count - 1/* || isindex<99*/) && (c
                                == "n" || c == "next"))
                        {
                            isindex++;
                            cout << endl << "--------- Initial state ---------"
                                    << endl;
                            print_state(inistates[isindex], *v);
                            //inistates[isindex].print(2, 2);
                            cout << "----------------------------" << endl;
                        }
                        else if (isindex > 0 && (c == "p" || c == "previous"))
                        {
                            isindex--;
                            cout << endl << "--------- Initial state ---------"
                                    << endl;
                            print_state(inistates[isindex], *v);
                            //inistates[isindex].print(2, 2);
                            cout << "----------------------------" << endl;
                        }
                        else if (c == "e" || c == "exit")
                            exit(0);
                        else
                            cout << "Please choose one option!" << endl;
                    }
                }
                stack[sp++] = inistates[isindex]; // initial state
                while (true)
                {
                    BDDvector enabled(MAXTRANSITIONS, bddmgr);
                    int tcount = 0;
                    BDD newstates;
                    int tran = -2;
                    if (sp >= MAXSTACKDEPTH)
                    {
                        while (tran != -1 && tran != 0)
                        {
                            cout
                                    << "Maximum stack depth is reached. Please type 0 to backtrack or -1 to quit immediately: ";
                            cin >> tran;
                        }
                    }
                    else
                    {
                        if (options["debug"] == 1 && options["verbosity"] > 10)
                        {
                            cout << "newstate: ";
                            stack[sp - 1].print(2, 2);
                        }
                        newstates = stack[sp - 1];// next state
                        for (unsigned int k = 0; k < agents->size(); k++)
                            newstates *= (*vRT)[k];
                        if (options["debug"] == 1 && options["verbosity"] > 10)
                        {
                            cout << "newstate + trans: ";
                            newstates.print(2, 2);
                        }
                        BDD transitions = newstates;
                        if (newstates != bddmgr->bddZero())
                        {
                            while (tcount < MAXTRANSITIONS && transitions
                                    != bddmgr->bddZero())
                            {
                                enabled[tcount]
                                        = transitions.PickOneMinterm(*a);
                                transitions -= enabled[tcount];
                                if (is_valid_action(enabled[tcount], *a))
                                    tcount++;
                            }
                        }
                        if (tcount == MAXTRANSITIONS && transitions
                                != bddmgr->bddZero())
                            cout
                                    << "There are too many enabled transitions. We only pick up 100 of them."
                                    << endl;
                        if (tcount > 0)
                        {
                            cout << "Enabled transtions: " << endl;
                            for (int i = 0; i < tcount; i++)
                            {
                                cout << i + 1 << " : ";
                                print_action(enabled[i], *a);
                            }
                            while (tran < -1 || tran > tcount)
                            {
                                cout
                                        << "Please choose one, or type 0 to backtrack or -1 to quit: "
                                        << endl;
                                cin >> tran;
                            }
                        }
                        else
                        {
                            if (sp > 1 || count > 1)
                            {
                                cout
                                        << "There is no enabled transition. Please type 0 to backtrack or -1 to quit immediately: ";
                                cin >> tran;
                                while (tran != -1 && tran != 0)
                                {
                                    cout
                                            << "Maximum stack depth is reached. Please type 0 to backtrack or -1 to quit immediately: ";
                                    cin >> tran;
                                }
                            }
                            else
                            {
                                cout
                                        << "There is no enabled transition in the initial state. Simulation exits."
                                        << endl;
                                exit(0);
                            }
                        }
                    }
                    if (tran == -1)
                        exit(0);
                    else if (tran == 0 && sp > 1)
                    {
                        stack[--sp] = bddmgr->bddZero();
                        continue;
                    }
                    else if (tran == 0 && sp == 1)
                    {
                        stack[--sp] = bddmgr->bddZero();
                        break;
                    }
                    else
                    {
                        newstates *= enabled[tran - 1];
                        if (options["debug"] == 1 && options["verbosity"] > 10)
                        {
                            cout << "newstate: ";
                            newstates.print(2, 2);
                        }
                        BDD tmpstate = Exists(v, newstates); // clear state variables
                        tmpstate = tmpstate.SwapVariables(*v, *pv);
                        tmpstate = Exists(a, tmpstate); // clear action variables
                        tmpstate = append_variable_BDDs(tmpstate);
                        //BDD tmpback = tmpstate;
                        int count1 = 0;
                        BDDvector succstates(MAXINISTATES, bddmgr);
                        statehash.clear();
                        while (count1 < MAXINISTATES && tmpstate
                                != bddmgr->bddZero())
                        {
                            succstates[count1] = tmpstate.PickOneMinterm(*v);
                            tmpstate = tmpstate - succstates[count1];
                            if (is_valid_state(succstates[count1], *v))
                            {
                                string state = state_to_str(succstates[count1],
                                        *v);
                                if (!find_same_state(&statehash, state))
                                {
                                    statehash[state] = 1;
                                    count1++;
                                }
                            }
                        }
                        if (count1 == MAXINISTATES && tmpstate
                                != bddmgr->bddZero())
                            cout
                                    << "There are too many states. Please refine your model."
                                    << endl;
                        else if (count1 > 1)
                            cout << "Warning: there are many states." << endl;
                        cout << endl << "--------- Current state ---------"
                                << endl;
                        int succindex = 0;
                        print_state(succstates[succindex], *v);
                        cout << "----------------------------" << endl;
                        if (count1 > 1)
                        {
                            bool choose = false;
                            string c;
                            while (!choose)
                            {
                                if (succindex == 0)
                                    cout
                                            << "Is this the current state? [Y(es), N(ext), E(xit)]: ";
                                else if (succindex == count1 - 1)
                                    cout
                                            << "Is this the current state? [Y(es), P(revious), E(xit)]: ";
                                else
                                    cout
                                            << "Is this the current state? [Y(es), N(ext), P(revious), E(xit)]: ";
                                cin >> c;
                                transform(c.begin(), c.end(), c.begin(),
                                        (int(*)(int)) tolower);
                                if (c == "y" || c == "yes")
                                {
                                    choose = true;
                                    break;
                                }
                                else if ((succindex < count1 - 1/* || succindex<99*/)
                                        && (c == "n" || c == "next"))
                                {
                                    succindex++;
                                    cout << endl
                                            << "--------- Current state ---------"
                                            << endl;
                                    print_state(succstates[succindex], *v);
                                    //succstates[succindex].print(2, 2);
                                    cout << "----------------------------"
                                            << endl;
                                }
                                else if (succindex > 0 && (c == "p" || c
                                        == "previous"))
                                {
                                    succindex--;
                                    cout << endl
                                            << "--------- Initial state ---------"
                                            << endl;
                                    print_state(succstates[succindex], *v);
                                    //succstates[succindex].print(2, 2);
                                    cout << "----------------------------"
                                            << endl;
                                }
                                else if (c == "e" || c == "exit")
                                    exit(0);
                                else
                                    cout << "Please choose one option!" << endl;
                            }
                        }
                        stack[sp++] = succstates[succindex];
                        //sp++;
                    }
                }
            }
        }
        else
        {
            while (true)
            {
                BDDvector stack(MAXSTACKDEPTH, bddmgr);
                int sp = 0;
                for (int k = 0; k < count; k++)
                {
                    cout << endl << "-- State " << (k + 1) << " --" << endl;
                    print_state(inistates[k], *v);
                }
                cout << "Done." << endl;
                int isindex = 0;
                ;
                cin >> isindex;
                if (isindex == -1)
                    exit(0);
                stack[sp++] = inistates[isindex - 1]; // initial state
                while (true)
                {
                    BDDvector enabled(MAXTRANSITIONS, bddmgr);
                    int tcount = 0;
                    BDD newstates;
                    int tran = -2;
                    if (sp >= MAXSTACKDEPTH)
                    {
                        while (tran != -1 && tran != 0)
                        {
                            cout
                                    << "Maximum stack depth is reached. Please backtrack or quit.";
                            cin >> tran;
                        }
                    }
                    else
                    {
                        newstates = stack[sp - 1];// next state
                        for (unsigned int k = 0; k < agents->size(); k++)
                            newstates *= (*vRT)[k];
                        BDD transitions = newstates;
                        if (newstates != bddmgr->bddZero())
                        {
                            while (tcount < MAXTRANSITIONS && transitions
                                    != bddmgr->bddZero())
                            {
                                enabled[tcount]
                                        = transitions.PickOneMinterm(*a);
                                transitions -= enabled[tcount];
                                if (is_valid_action(enabled[tcount], *a))
                                    tcount++;
                            }
                        }
                        if (tcount > 0)
                        {
                            //cout << "Enabled transtions: "<< endl;
                            for (int i = 0; i < tcount; i++)
                            {
                                cout << "-- transition " << (i + 1) << " --"
                                        << endl;
                                print_action_1(enabled[i], *a);
                            }
                            cout << "Done." << endl;
                            while (tran < -1 || tran > tcount)
                            {
                                cin >> tran;
                            }
                        }
                        else
                        {
                            if (sp > 1 || count > 1)
                            {
                                cout
                                        << "There is no enabled transition. Please backtrack or quit.";
                                cin >> tran;
                            }
                            else
                            {
                                cout
                                        << "There is no enabled transition in the initial state."
                                        << endl;
                                exit(0);
                            }
                        }
                    }
                    if (tran == -1)
                        exit(0);
                    else if (tran == 0 && sp > 1)
                    {
                        stack[--sp] = bddmgr->bddZero();
                        continue;
                    }
                    else if (tran == 0 && sp == 1)
                    {
                        stack[--sp] = bddmgr->bddZero();
                        break;
                    }
                    else
                    {
                        newstates *= enabled[tran - 1];
                        BDD tmpstate = Exists(v, newstates); // clear state variables
                        tmpstate = tmpstate.SwapVariables(*v, *pv);
                        tmpstate = Exists(a, tmpstate); // clear action variables
                        tmpstate = append_variable_BDDs(tmpstate);
                        //BDD tmpback = tmpstate;
                        int count1 = 0;
                        BDDvector succstates(MAXINISTATES, bddmgr);
                        statehash.clear();
                        while (count1 < MAXINISTATES && tmpstate
                                != bddmgr->bddZero())
                        {
                            succstates[count1] = tmpstate.PickOneMinterm(*v);
                            tmpstate = tmpstate - succstates[count1];
                            if (is_valid_state(succstates[count1], *v))
                            {
                                string state = state_to_str(succstates[count1],
                                        *v);
                                if (!find_same_state(&statehash, state))
                                {
                                    statehash[state] = 1;
                                    count1++;
                                }
                            }
                        }
                        for (int k = 0; k < count1; k++)
                        {
                            cout << endl << "-- State " << (k + 1) << " --"
                                    << endl;
                            print_state(succstates[k], *v);
                        }
                        cout << "Done." << endl;
                        int succindex = 0;
                        cin >> succindex;
                        if (succindex == -1)
                            exit(0);
                        if (succindex > 0)
                            stack[sp++] = succstates[succindex - 1];
                        //sp++;
                    }
                }
            }
        }
    }
}

void experiment_0(void)
{

    Cudd_ReorderingType REORDERING = CUDD_REORDER_GROUP_SIFT_CONV;

    if (options["initialfirst"] == 1)
    {
        if (options["quiet"] == 0 || options["simulation"] == 0)
        {
            cout << "  Building OBDD for initial states..." << endl;
        }
        in_st
                = (options["flatexpression"] < 2) ? is_istates->encode_bdd(
                        bddOne) : is_istates->encode_bdd_flat(bddOne);
        in_st = append_variable_BDDs(in_st);
        if (options["optimization"] == 1 || options["optimization"] == 2)
            MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), REORDERING);
        if (options["verbosity"] > 3)
        {
            cout << "Done." << endl;
        }
    }

    if (options["quiet"] == 0 || options["simulation"] == 0)
        cout << "Building OBDDs for protocols..." << endl;

    andprot = bddmgr->bddOne();
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        if (options["verbosity"] > 3)
        {
            if (i == 0)
                cout << endl;
            cout << "      Processing " << (*agents)[i]->get_name() << endl;
        }
        andprot *= (*agents)[i]->encode_protocol();
    }

    if (options["quiet"] == 0 || options["simulation"] == 0)
    {
        cout << "Building OBDDs for evolution functions..." << endl;
    }

    // Encode evolution functions
    preRT = bddmgr->bddOne();

    // REORDERING OF VARIABLES (forcing it):
    MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), REORDERING);

    for (unsigned int i = 0; i < agents->size(); i++)
    {
        if (options["verbosity"] > 3)
        {
            if (i == 0)
                cout << endl;
            cout << "      Processing " << (*agents)[i]->get_name() << endl;
        }
        preRT *= (*agents)[i]->encode_evolution();
        //MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_GROUP_SIFT_CONV);
    }

    if (options["quiet"] == 0 || options["simulation"] == 0)
    {
        cout << "Building OBDD for global transition relation..." << endl;
    }

    MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);

    //BDD trans = bddmgr->bddOne();
    trans = preRT * andprot;
    RT = Exists(a, trans);
    if (options["verbosity"] > 3)
    {
        cout << "Done." << endl;
    }

    if (options["initialfirst"] == 0)
    {
        if (options["quiet"] == 0 || options["simulation"] == 0)
        {
            cout << "Building OBDD for initial states..." << endl;
        }
        in_st
                = (options["flatexpression"] < 2) ? is_istates->encode_bdd(
                        bddOne) : is_istates->encode_bdd_flat(bddOne);
        in_st = append_variable_BDDs(in_st);
        if (options["verbosity"] > 3)
        {
            cout << "Done." << endl;
        }
    }

    // REORDERING OF VARIABLES (forcing):
    REORDERING = CUDD_REORDER_WINDOW4_CONV;
    MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), REORDERING);
    //MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);

    if (options["quiet"] == 0 || options["simulation"] == 0)
    {
        cout << "Building OBDD for reachable states..." << endl;
    }

    reach = bddmgr->bddZero();
    BDD q = in_st;
    BDD next = bddmgr->bddZero();
    int acounter = 1;

    if (options["verbosity"] > 9)
    {
        cout << endl;
    }

    while (q != reach)
    {
        if (options["verbosity"] > 5)
        {
            cout << "    Computing depth " << acounter << endl;
        }
        reach = q;
        if (options["verbosity"] > 9)
        {
            cout << "Before evolution: " << endl;
            Exists(a, reach).print(2, 2);
        }
        next = Exists(v, q * RT);
        next = next.SwapVariables(*v, *pv);
        //next = append_variable_BDDs(next);
        //next = Exists(a, next); // Clear actions.

        if (options["verbosity"] > 9)
        {
            cout << "Next states: " << endl;
            next.print(2, 2);
        }
        //next = next * andprot; // syncronize actions with local states
        q = q + next;
        //if ( options["debug"] == 1 ) {
        if (options["verbosity"] > 9)
        {
            cout << "Press enter to continue" << endl;
            char c;
            cin.get(c);
        }
        acounter++;
    }

    reach = Exists(a, reach);
}

void experiment_1(void)
{
    reach = bddmgr->bddZero();
    BDD q1 = in_st;
    BDD next1 = bddmgr->bddZero();
    int acounter1 = 1;

    //time_t t21 = time( 0 );
    while (q1 != reach)
    {
        if (options["verbosity"] > 5)
            cout << "    Computing depth " << acounter1 << endl;

        reach = q1;
        if (options["verbosity"] > 9)
        {
            cout << "Before evolution: " << endl;
            Exists(a, reach).print(2, 2);
        }
        //next1 = Exists(v, q*RT);
        next1 = q1;
        for (unsigned int k = 0; k < agents->size(); k++)
            next1 *= (*vRT)[k];
        next1 = Exists(v, next1);
        next1 = next1.SwapVariables(*v, *pv);
        //next = append_variable_BDDs(next);
        next1 = Exists(a, next1); // Clear actions.

        if (options["verbosity"] > 9)
        {
            cout << "Next states: " << endl;
            next1.print(2, 2);
        }
        //next = next * andprot; // syncronize actions with local states
        //if(!(next1<=q1))
        q1 = q1 + next1;
        //MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
        //if ( options["debug"] == 1 ) {
        if (options["verbosity"] > 9)
        {
            cout << "Press enter to continue" << endl;
            char c;
            cin.get(c);
        }
        acounter1++;
    }

    reach = Exists(a, reach);

    if (options["verbosity"] > 3)
    {
        cout << "Done" << endl;
    }
}

void experiment_2(void)
{
    cout << "<E2>" << endl;
    // BMC goes here
    options["bddcache"] = 0;

#if FORCED_REORDER
    Cudd_AutodynDisable(bddmgr->getManager());
    Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
    MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

#if REORDER_OFF
    Cudd_AutodynDisable(bddmgr->getManager());
#endif

    reach = in_st;
    BDD q1 = bddmgr->bddZero();
    BDD next1 = in_st;
    int acounter1 = 1;
    int i = 0;
    int pre, post;
    pre = bddmgr->ReadMemoryInUse();
    post = bddmgr->ReadMemoryInUse();
    double prestates, poststates;
    prestates = reach.CountMinterm(v->count());
    poststates = reach.CountMinterm(v->count());
    while (true)
    {
        cout << "Depth " << i << endl;
        ++i;

        cout << pre << "," << post << "," << (post - pre) << endl;
        cout << prestates << "," << poststates << "," << (poststates
                - prestates) << endl;
        pre = post;
        prestates = poststates;

        if (options["verbosity"] > 5)
            cout << "    Computing depth " << acounter1 << endl;

        if (options["verbosity"] > 9)
        {
            cout << "Before evolution: " << endl;
            Exists(a, reach).print(2, 2);
        }
        for (unsigned int k = 0; k < agents->size(); k++)
            next1 *= (*vRT)[k];
        next1 = Exists(v, next1);
        next1 = next1.SwapVariables(*v, *pv);
        next1 = Exists(a, next1); // Clear actions.

#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        if (options["verbosity"] > 9)
        {
            cout << "Next states: " << endl;
            next1.print(2, 2);
        }
        q1 = reach + next1;

#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        if (options["verbosity"] > 9)
        {
            cout << "Press enter to continue" << endl;
            char c;
            cin.get(c);
        }
        acounter1++;

        //        unsigned long memoryinuse = bddmgr->ReadMemoryInUse();
        //        cout << "Meminfo = " << memoryinuse << endl;

        if (q1 == reach)
            break;
        else
            reach = q1;

        post = bddmgr->ReadMemoryInUse();
        poststates = reach.CountMinterm(v->count());
    }

    pre = bddmgr->ReadMemoryInUse();
    post = bddmgr->ReadMemoryInUse();
    cout << pre << "," << post << "," << (post - pre) << endl;
    cout << prestates << "," << poststates << "," << (poststates - prestates)
            << endl;

    if (options["verbosity"] > 3)
    {
        cout << "Done" << endl;
    }
    cout << "</E2>" << endl;
}

void experiment_3(void)
{

    reach = in_st;
    BDD next1 = in_st;
    int acounter1 = 1;
    while (true)
    {
        if (options["verbosity"] > 5)
            cout << "    Computing depth " << acounter1 << endl;

        if (options["verbosity"] > 9)
        {
            cout << "Before evolution: " << endl;
            Exists(a, reach).print(2, 2);
        }
        for (unsigned int k = 0; k < agents->size(); k++)
            next1 *= (*vRT)[k];
        next1 = Exists(v, next1);
        next1 = next1.SwapVariables(*v, *pv);
        next1 = Exists(a, next1); // Clear actions.
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);

        if (options["verbosity"] > 9)
        {
            cout << "Next states: " << endl;
            next1.print(2, 2);
        }
        next1 = next1 - reach;
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);

        if (options["verbosity"] > 9)
        {
            cout << "Press enter to continue" << endl;
            char c;
            cin.get(c);
        }
        acounter1++;

        if (next1 == bddmgr->bddZero())
            break;
        else
            reach = reach + next1;
        if (options["verbosity"] > 3)
        {
            cout << "Done" << endl;
        }
    }

}

void experiment_4(void)
{
    cout << "<E4>" << endl;
    options["bddcache"] = 0;

#if FORCED_REORDER
    Cudd_AutodynDisable(bddmgr->getManager());
    Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
    MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

#if REORDER_OFF
    Cudd_AutodynDisable(bddmgr->getManager());
#endif

    // BMC goes here
    reach = in_st;
    //print_state(in_st, *v);
    //in_st = bddmgr->bddZero();
    //print_state(in_st, *v);

    /* Test writing BDDs to a file and restoring it */
#if 0
    char ** varmatchnames=NULL; /* array of variable names (accessed by ids) */
    int * varmatchauxids=NULL; /* array of variable auxids (accessed by ids) */
    int * varcomposeids=NULL; /* array of new ids (accessed by ids) */
    Dddmp_VarMatchType varmatchmode;
    Dddmp_VarInfoType varoutinfo;
    varmatchmode = DDDMP_VAR_MATCHIDS;
    varoutinfo = DDDMP_VARIDS;
    int status;
    char filename[100];
    strcpy(filename,"Helloworld.out");
    BDD out, in;

    out = in_st;
    in = in_st;
    //cout << "equal? " << (out == in ? "True" : "False") << endl;

    {
        BDD temp = in_st;
        DdNode* a = (reach.getNode());
        status = Dddmp_cuddBddStore(bddmgr->getManager(), NULL, a, varmatchnames, varmatchauxids,
                DDDMP_MODE_TEXT, varoutinfo, filename, NULL);

        //Dddmp_cuddBddStore(NULL, NULL, NULL, NULL, NULL, NULL, varoutinfo, NULL, NULL);

        //print_state(temp, *v);
        //cout << endl;
        out = temp;
    }

    {
        DdNode* b;
        b = Dddmp_cuddBddLoad(bddmgr->getManager(), varmatchmode, varmatchnames, varmatchauxids,
                varcomposeids, DDDMP_MODE_DEFAULT, filename, NULL);
        BDD temp(bddmgr, b);
        //print_state(temp, *v);
        //cout << endl;

        reach = temp;
        in = temp;
    }

    //cout << "equal? " << (out == in ? "True" : "False") << endl;


    //exit(-1);
#endif

    BDD q1 = bddmgr->bddZero();
    BDD next1 = in_st;
    int acounter1 = 1;
    int i = 0;
    int pre, post;
    pre = bddmgr->ReadMemoryInUse();
    post = bddmgr->ReadMemoryInUse();
    double prestates, poststates;
    prestates = reach.CountMinterm(v->count());
    poststates = reach.CountMinterm(v->count());
    while (!bmc_formulae->empty())
    {
        cout << "Checking at depth " << i << endl;
        cout << pre << "," << post << "," << (post - pre) << endl;
        cout << prestates << "," << poststates << "," << (poststates
                - prestates) << endl;
        pre = post;
        prestates = poststates;

        //unsigned long memoryinuse = bddmgr->ReadMemoryInUse();
        // cout << "BDD memory in use = " << memoryinuse << endl;

        //pre = bddmgr->ReadMemoryInUse();
        /*
         if (i && (i % 20 == 0))
         {
         */
        check_formulae_BMC();
        //if (i == 20) break;
        /*
         post = bddmgr->ReadMemoryInUse();

         cout << pre << "," << post << "," << (post - pre) << endl;
         break;
         }
         */
        //post = bddmgr->ReadMemoryInUse();
        //pre = bddmgr->ReadMemoryInUse();
        //Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
        //post = bddmgr->ReadMemoryInUse();
#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        //cout << pre << "," << post << "," << (post - pre) << endl;

        if (bmc_formulae->empty())
            continue;

        /*
         memoryinuse -= bddmgr->ReadMemoryInUse();
         if (memoryinuse != 0)
         {
         cout << "Different " << memoryinuse << endl;
         }
         */
        ++i;

        if (options["verbosity"] > 5)
            cout << "    Computing depth " << acounter1 << endl;

        if (options["verbosity"] > 9)
        {
            cout << "Before evolution: " << endl;
            Exists(a, reach).print(2, 2);
        }
        for (unsigned int k = 0; k < agents->size(); k++)
            next1 *= (*vRT)[k];
        next1 = Exists(v, next1);
        next1 = next1.SwapVariables(*v, *pv);
        next1 = Exists(a, next1); // Clear actions.

#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        if (options["verbosity"] > 9)
        {
            cout << "Next states: " << endl;
            next1.print(2, 2);
        }
        q1 = reach + next1;

#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        if (options["verbosity"] > 9)
        {
            cout << "Press enter to continue" << endl;
            char c;
            cin.get(c);
        }
        acounter1++;

        if (q1 == reach)
        {
            cout << "Fix point reached" << endl;
            break;
        }
        else
            reach = q1;

        post = bddmgr->ReadMemoryInUse();
        poststates = reach.CountMinterm(v->count());
    }

    pre = bddmgr->ReadMemoryInUse();
    post = bddmgr->ReadMemoryInUse();
    cout << pre << "," << post << "," << (post - pre) << endl;
    cout << prestates << "," << poststates << "," << (poststates - prestates)
            << endl;

    // When we reach here
    // We either reched a fix point of the state space
    // Or Disproved all of the formulae

    if (bmc_false_formulae->size())
    {
        cout
                << "The following formulae have been verified using BMC on the negation:"
                << endl;
        int test = 0;
        for (modal_formula_p_pair_vector::iterator iter =
                bmc_false_formulae->begin(); iter != bmc_false_formulae->end(); ++iter)
        {
            modal_formula_p_pair temp = (modal_formula_p_pair) (*iter);
            modal_formula actl = *temp.first;

            cout << "  Formula " << actl.to_string()
                    << " is FALSE in the model" << endl;
            //            no_kbar = true;
            //            build_cex(&actl, test);
            ////            //check_formulae();
            ////            no_kbar = false;
            ++test;
        }
    }

    if (!bmc_formulae->empty()) // If we have remaining unchecked formulae
    {
        is_formulae->clear(); // Remove all the old formulae

        for (modal_formula_p_pair_vector::iterator iter = bmc_formulae->begin(); iter
                != bmc_formulae->end(); ++iter)
        {
            modal_formula_p_pair temp = (modal_formula_p_pair) (*iter);
            modal_formula actl = *temp.first;
            is_formulae->push_back(actl);
            //            no_kbar = true;
            //
            //            build_cex(&actl, 0);
            //            //check_formulae();
            //            no_kbar = false;
        }

        // Use the regular check_formulae method
        check_formulae();

    }

    if (options["verbosity"] > 3)
    {
        cout << "Done" << endl;
    }
    cout << "</E4>" << endl;
}

void experiment_5_Master(void)
{
    cout << "<E5 Master>" << endl;
    options["bddcache"] = 0;

#if FORCED_REORDER
    Cudd_AutodynDisable(bddmgr->getManager());
    Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
    MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

#if REORDER_OFF
    Cudd_AutodynDisable(bddmgr->getManager());
#endif

    // BMC goes here
    reach = in_st;

    /* Test writing BDDs to a file and restoring it */
#if 1
    char ** varmatchnames = NULL; /* array of variable names (accessed by ids) */
    int * varmatchauxids = NULL; /* array of variable auxids (accessed by ids) */
    int * varcomposeids = NULL; /* array of new ids (accessed by ids) */
    Dddmp_VarMatchType varmatchmode;
    Dddmp_VarInfoType varoutinfo;
    varmatchmode = DDDMP_VAR_MATCHIDS;
    varoutinfo = DDDMP_VARIDS;
    int status;
    char filename[100];
#endif

#if 0
    {
        BDD temp = in_st;
        DdNode* a = (reach.getNode());
        status = Dddmp_cuddBddStore(bddmgr->getManager(), NULL, a, varmatchnames, varmatchauxids,
                DDDMP_MODE_TEXT, varoutinfo, filename, NULL);

        //Dddmp_cuddBddStore(NULL, NULL, NULL, NULL, NULL, NULL, varoutinfo, NULL, NULL);

        print_state(temp, *v);
    }

    {
        DdNode* b;
        b = Dddmp_cuddBddLoad(bddmgr->getManager(), varmatchmode, varmatchnames, varmatchauxids,
                varcomposeids, DDDMP_MODE_DEFAULT, filename, NULL);
        BDD temp(bddmgr, b);
        print_state(temp, *v);

    }

    exit(-1);
#endif

    BDD q1 = bddmgr->bddZero();
    BDD next1 = in_st;
    int acounter1 = 1;
    int i = 0;
    int pre, post;
    pre = bddmgr->ReadMemoryInUse();
    post = bddmgr->ReadMemoryInUse();
    double prestates, poststates;
    prestates = reach.CountMinterm(v->count());
    poststates = reach.CountMinterm(v->count());
    while (!bmc_formulae->empty())
    {
        cout << "Checking at depth " << i << endl;
        cout << pre << "," << post << "," << (post - pre) << endl;
        cout << prestates << "," << poststates << "," << (poststates
                - prestates) << endl;
        pre = post;
        prestates = poststates;

        //unsigned long memoryinuse = bddmgr->ReadMemoryInUse();
        // cout << "BDD memory in use = " << memoryinuse << endl;

        //pre = bddmgr->ReadMemoryInUse();
        /*
         if (i && (i % 20 == 0))
         {
         */
        check_formulae_BMC();
        /*
         post = bddmgr->ReadMemoryInUse();

         cout << pre << "," << post << "," << (post - pre) << endl;
         break;
         }
         */
        //post = bddmgr->ReadMemoryInUse();
        //pre = bddmgr->ReadMemoryInUse();
        //Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
        //post = bddmgr->ReadMemoryInUse();
#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        //cout << pre << "," << post << "," << (post - pre) << endl;

        if (bmc_formulae->empty())
            continue;

        /*
         memoryinuse -= bddmgr->ReadMemoryInUse();
         if (memoryinuse != 0)
         {
         cout << "Different " << memoryinuse << endl;
         }
         */

        ++i;

        if (options["verbosity"] > 5)
            cout << "    Computing depth " << acounter1 << endl;

        if (options["verbosity"] > 9)
        {
            cout << "Before evolution: " << endl;
            Exists(a, reach).print(2, 2);
        }
        for (unsigned int k = 0; k < agents->size(); k++)
            next1 *= (*vRT)[k];
        next1 = Exists(v, next1);
        next1 = next1.SwapVariables(*v, *pv);
        next1 = Exists(a, next1); // Clear actions.

        /* Looping over states to find sucessors */
#if 1
        double nextcount = next1.CountMinterm(v->count());
        double currentstates = reach.CountMinterm(v->count());

        cout << endl << i << endl;

        if (i == one_shot_depth && !bmc_formulae->empty() /*nextcount >= 100*/)
        {
            BDD nextstates = next1;

            int divisor = (int) (nextcount / 5000.0f);
            cout << "Next count : " << nextcount << ", Divisor: " << divisor
                    << "." << endl;

            cout << "\n\n\n\n" << endl;
            cout << "**** EXPERIMENT 5 ****" << endl;
            cout << "Generating seeds" << endl;
            cout << "Temporary directory: " << "temp_bdds/" << endl;
            cout << "Generated seeds: " << nextcount << endl;
            cout << "Memory consumed: " << bddmgr->ReadMemoryInUse() << endl;
            cout << "Reachable states: " << currentstates << endl;

            //            cout << "<PRINTING> ......" << endl;
            //
            int state_iter = 0;
            while (nextstates != bddmgr->bddZero())
            {
                BDD singlenextstate = nextstates.PickOneMinterm(*v);
                if (!is_valid_state(singlenextstate, *v))
                    continue;
                //if (!(state_iter % divisor))
                {
                    strcpy(filename, "");
                    sprintf(filename, "temp_bdds/state_%04d.out", state_iter);
                    //strcpy(filename,"Helloworld.out");
                    //cout << state_iter << endl;
                    //cout << "<STATE>" << endl;
                    DdNode* a = (singlenextstate.getNode());

                    status = Dddmp_cuddBddStore(bddmgr->getManager(), NULL, a,
                            varmatchnames, varmatchauxids, DDDMP_MODE_TEXT,
                            varoutinfo, filename, NULL);

                    // print_state(singlenextstate, *v);
                    //cout << "</STATE>\n" << endl;
                }
                nextstates -= singlenextstate;
                state_iter++;
            }

            if (atomic_k_bar_formula)
            {
                BDD k_bar_states = atomic_k_bar_formula->check_formula();

                strcpy(filename, "");
                sprintf(filename, "temp_bdds/atomic_k_bar_states.out");

                DdNode* a = (k_bar_states.getNode());

                status = Dddmp_cuddBddStore(bddmgr->getManager(), NULL, a,
                        varmatchnames, varmatchauxids, DDDMP_MODE_TEXT,
                        varoutinfo, filename, NULL);
            }

            cout << "Memory consumed: " << bddmgr->ReadMemoryInUse() << endl;
            //
            exit(0);
            //            cout << "...... </PRINTING>\n" << endl;
        }
#endif

#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        if (options["verbosity"] > 9)
        {
            cout << "Next states: " << endl;
            next1.print(2, 2);
        }
        q1 = reach + next1;

#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        if (options["verbosity"] > 9)
        {
            cout << "Press enter to continue" << endl;
            char c;
            cin.get(c);
        }
        acounter1++;

        if (q1 == reach)
        {
            //cout << "Fix point reached" << endl;
            break;
        }
        else
            reach = q1;

        post = bddmgr->ReadMemoryInUse();
        poststates = reach.CountMinterm(v->count());
    }

    pre = bddmgr->ReadMemoryInUse();
    post = bddmgr->ReadMemoryInUse();
    cout << pre << "," << post << "," << (post - pre) << endl;
    cout << prestates << "," << poststates << "," << (poststates - prestates)
            << endl;

    // When we reach here
    // We either reched a fix point of the state space
    // Or Disproved all of the formulae

    if (bmc_false_formulae->size())
    {
        cout
                << "The following formulae have been verified using BMC on the negation:"
                << endl;

        for (modal_formula_p_pair_vector::iterator iter =
                bmc_false_formulae->begin(); iter != bmc_false_formulae->end(); ++iter)
        {
            modal_formula_p_pair temp = (modal_formula_p_pair) (*iter);
            modal_formula actl = *temp.first;

            cout << "  Formula " << actl.to_string()
                    << " is FALSE in the model" << endl;
        }
    }

    if (!bmc_formulae->empty()) // If we have remaining unchecked formulae
    {
        is_formulae->clear(); // Remove all the old formulae

        for (modal_formula_p_pair_vector::iterator iter = bmc_formulae->begin(); iter
                != bmc_formulae->end(); ++iter)
        {
            modal_formula_p_pair temp = (modal_formula_p_pair) (*iter);
            modal_formula actl = *temp.first;
            is_formulae->push_back(actl);
        }

        // Use the regular check_formulae method
        check_formulae();

    }

    if (options["verbosity"] > 3)
    {
        cout << "Done" << endl;
    }

    cout << "\n\n\n\n" << endl;
    cout << "**** EXPERIMENT 5 ****" << endl;
    cout << "Verification complete" << endl;
    cout << (!bmc_formulae->empty() ? "TRUE" : "FALSE") << endl;
    cout << "Memory consumed: " << bddmgr->ReadMemoryInUse() << endl;
    cout << "Reachable states: " << poststates << endl;

    exit(0);

    //cout << "</E5 Master>" << endl;
}
void experiment_5_Slave(void)
{
    cout << "<E5 Slave>" << endl;

    char ** varmatchnames = NULL; /* array of variable names (accessed by ids) */
    int * varmatchauxids = NULL; /* array of variable auxids (accessed by ids) */
    int * varcomposeids = NULL; /* array of new ids (accessed by ids) */
    Dddmp_VarMatchType varmatchmode;
    Dddmp_VarInfoType varoutinfo;
    varmatchmode = DDDMP_VAR_MATCHIDS;
    varoutinfo = DDDMP_VARIDS;
    int status;
    char filename[100];
    strcpy(filename, initbddfile.c_str());

    DdNode* b;
    b = Dddmp_cuddBddLoad(bddmgr->getManager(), varmatchmode, varmatchnames,
            varmatchauxids, varcomposeids, DDDMP_MODE_DEFAULT, filename, NULL);
    BDD temp(bddmgr, b);
    //print_state(temp, *v);

    options["bddcache"] = 0;

#if FORCED_REORDER
    Cudd_AutodynDisable(bddmgr->getManager());
    Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
    MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

#if REORDER_OFF
    Cudd_AutodynDisable(bddmgr->getManager());
#endif

    // BMC goes here
    //in_st = bddmgr->bddZero();
    //print_state(in_st, *v);
    in_st = temp;
    //print_state(in_st, *v);
    reach = temp;
    //reach = temp;

    BDD q1 = bddmgr->bddZero();
    BDD next1 = temp;
    int acounter1 = 1;
    int i = 0;
    int pre, post;
    pre = bddmgr->ReadMemoryInUse();
    post = bddmgr->ReadMemoryInUse();
    double prestates, poststates;
    prestates = reach.CountMinterm(v->count());
    poststates = reach.CountMinterm(v->count());
    while (!bmc_formulae->empty())
    {
        cout << "Checking at depth " << i << endl;
        //        cout << pre << "," << post << "," << (post - pre) << endl;
        //        cout << prestates << "," << poststates << "," << (poststates
        //                - prestates) << endl;
        pre = post;
        prestates = poststates;

        check_formulae_BMC();

#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        if (bmc_formulae->empty())
            continue;

        ++i;

        if (options["verbosity"] > 5)
            cout << "    Computing depth " << acounter1 << endl;

        if (options["verbosity"] > 9)
        {
            cout << "Before evolution: " << endl;
            Exists(a, reach).print(2, 2);
        }
        for (unsigned int k = 0; k < agents->size(); k++)
            next1 *= (*vRT)[k];
        next1 = Exists(v, next1);
        next1 = next1.SwapVariables(*v, *pv);
        next1 = Exists(a, next1); // Clear actions.

#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        if (options["verbosity"] > 9)
        {
            cout << "Next states: " << endl;
            next1.print(2, 2);
        }
        q1 = reach + next1;

#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        if (options["verbosity"] > 9)
        {
            cout << "Press enter to continue" << endl;
            char c;
            cin.get(c);
        }
        acounter1++;

        if (q1 == reach)
        {
            cout << "Fix point reached" << endl;
            break;
        }
        else
            reach = q1;

        post = bddmgr->ReadMemoryInUse();
        poststates = reach.CountMinterm(v->count());
    }
    check_formulae_BMC();
    //    pre = bddmgr->ReadMemoryInUse();
    //    post = bddmgr->ReadMemoryInUse();
    //    cout << pre << "," << post << "," << (post - pre) << endl;
    //    cout << prestates << "," << poststates << "," << (poststates - prestates)
    //            << endl;

    // When we reach here
    // We either reched a fix point of the state space
    // Or Disproved all of the formulae

    cout << i << "," << post << "," << poststates << endl;

    if (bmc_formulae->empty())
    {
        cout << "CEX found from this init state" << endl;
        //cout << initbddfile << "\tWin\t" << i << "\t" << poststates << "\t" << post << endl;
    }
    else
    {
        cout << "Loading atomic k_bar states ..." << endl;
        // Last ditch attempt ...
        sprintf(filename, "temp_bdds/atomic_k_bar_states.out");

        // Load the k_bar states
        DdNode* kb;
        kb = Dddmp_cuddBddLoad(bddmgr->getManager(), varmatchmode, varmatchnames,
                varmatchauxids, varcomposeids, DDDMP_MODE_DEFAULT, filename, NULL);
        BDD kb_states(bddmgr, kb);
        
        // Or them onto the current reach set
        reach = reach + kb_states;

        // Check the K_bar a final time
        check_formulae_BMC();

        // If we've solved the formulae, then wonderful ...
        if (bmc_formulae->empty())
        {
            cout << "CEX found from this init state" << endl;
            //cout << initbddfile << "\tWin\t" << i << "\t" << poststates << "\t" << post << endl;
        }
        else
        {
            // Otherwise it looks like it's true
            cout << "as far as we're aware, the formulae is true for this state."
            << endl;
        }

        post = bddmgr->ReadMemoryInUse();
        poststates = reach.CountMinterm(v->count());
    }
    //    else
    //    {
    //        cout << initbddfile << "\tFail\t" << i << "\t" << poststates << "\t" << post << endl;
    //    }

    cout << "\n\n\n\n" << endl;
    cout << "**** EXPERIMENT 5 ****" << endl;
    cout << "Verification complete" << endl;
    cout << (!bmc_formulae->empty() ? "TRUE" : "FALSE") << endl;
    cout << "Memory consumed: " << bddmgr->ReadMemoryInUse() << endl;
    cout << "Reachable states: " << poststates << endl;

    exit(0);

#if 0
    if (bmc_false_formulae->size())
    {
        cout
        << "The following formulae have been verified using BMC on the negation:"
        << endl;

        for (modal_formula_p_pair_vector::iterator iter =
                bmc_false_formulae->begin(); iter != bmc_false_formulae->end(); ++iter)
        {
            modal_formula_p_pair temp = (modal_formula_p_pair) (*iter);
            modal_formula actl = *temp.first;

            cout << "  Formula " << actl.to_string()
            << " is FALSE in the model" << endl;
        }
    }

    if (!bmc_formulae->empty()) // If we have remaining unchecked formulae

    {
        is_formulae->clear(); // Remove all the old formulae

        for (modal_formula_p_pair_vector::iterator iter = bmc_formulae->begin(); iter
                != bmc_formulae->end(); ++iter)
        {
            modal_formula_p_pair temp = (modal_formula_p_pair) (*iter);
            modal_formula actl = *temp.first;
            is_formulae->push_back(actl);
        }

        // Use the regular check_formulae method

        cout << "We have be unable to disprove these formulae upto depth 10"
        << endl;
    }

    if (options["verbosity"] > 3)
    {
        cout << "Done" << endl;
    }
#endif
    cout << "</E5 Slave>" << endl;
}

void experiment_6(void)
{
    cout << "<E4>" << endl;
    options["bddcache"] = 0;

#if FORCED_REORDER
    Cudd_AutodynDisable(bddmgr->getManager());
    Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
    MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

#if REORDER_OFF
    Cudd_AutodynDisable(bddmgr->getManager());
#endif

    // BMC goes here
    reach = in_st;
    //print_state(in_st, *v);
    //in_st = bddmgr->bddZero();
    //print_state(in_st, *v);

    /* Test writing BDDs to a file and restoring it */

    BDD q1 = bddmgr->bddZero();
    BDD next1 = in_st;
    int acounter1 = 1;
    int i = 0;
    int pre, post;
    pre = bddmgr->ReadMemoryInUse();
    post = bddmgr->ReadMemoryInUse();
    double prestates, poststates;
    prestates = reach.CountMinterm(v->count());
    poststates = reach.CountMinterm(v->count());
    while (!bmc_formulae->empty())
    {
        cout << "Checking at depth " << i << endl;
        cout << pre << "," << post << "," << (post - pre) << endl;
        cout << prestates << "," << poststates << "," << (poststates
                - prestates) << endl;
        pre = post;
        prestates = poststates;

        //unsigned long memoryinuse = bddmgr->ReadMemoryInUse();
        // cout << "BDD memory in use = " << memoryinuse << endl;

        //pre = bddmgr->ReadMemoryInUse();
        /*
         if (i && (i % 20 == 0))
         {
         */
        /*else */
        if (i == one_shot_depth)
        {
            check_formulae_BMC();

            if (bmc_formulae->empty())
            {
                cout << "CEX found at " << one_shot_depth << endl;
            }
            else
            {
                cout << "CEX not found at " << one_shot_depth << endl;
            }

            cout << "adas" << endl;
            pre = bddmgr->ReadMemoryInUse();
            post = bddmgr->ReadMemoryInUse();
            cout << pre << "," << post << "," << (post - pre) << endl;
            cout << prestates << "," << poststates << "," << (poststates
                    - prestates) << endl;

            return;
        }

        //if (i == 20) break;
        /*
         post = bddmgr->ReadMemoryInUse();

         cout << pre << "," << post << "," << (post - pre) << endl;
         break;
         }
         */
        //post = bddmgr->ReadMemoryInUse();
        //pre = bddmgr->ReadMemoryInUse();
        //Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
        //post = bddmgr->ReadMemoryInUse();
#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        //cout << pre << "," << post << "," << (post - pre) << endl;

        //if (bmc_formulae->empty())
        //    continue;

        /*
         memoryinuse -= bddmgr->ReadMemoryInUse();
         if (memoryinuse != 0)
         {
         cout << "Different " << memoryinuse << endl;
         }
         */

        if (options["verbosity"] > 5)
            cout << "    Computing depth " << acounter1 << endl;

        if (options["verbosity"] > 9)
        {
            cout << "Before evolution: " << endl;
            Exists(a, reach).print(2, 2);
        }
        for (unsigned int k = 0; k < agents->size(); k++)
            next1 *= (*vRT)[k];
        next1 = Exists(v, next1);
        next1 = next1.SwapVariables(*v, *pv);
        next1 = Exists(a, next1); // Clear actions.

#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        if (options["verbosity"] > 9)
        {
            cout << "Next states: " << endl;
            next1.print(2, 2);
        }
        q1 = reach + next1;

#if FORCED_REORDER
        Cudd_ReduceHeap(bddmgr->getManager(), CUDD_REORDER_SIFT, 1);
#endif

#if AUTO_REORDER
        MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);
#endif

        if (options["verbosity"] > 9)
        {
            cout << "Press enter to continue" << endl;
            char c;
            cin.get(c);
        }
        acounter1++;

        if (q1 == reach)
        {
            cout << "Fix point reached" << endl;

            check_formulae_BMC();

            if (!bmc_formulae->empty())
            {
                cout << "Fix Point: TRUE " << endl;
            }
            else
            {
                cout << "Fix Point: FALSE " << endl;
            }

            pre = bddmgr->ReadMemoryInUse();
            post = bddmgr->ReadMemoryInUse();
            cout << pre << "," << post << "," << (post - pre) << endl;
            cout << prestates << "," << poststates << "," << (poststates
                    - prestates) << endl;

            return;

        }

        else
            reach = q1;

        ++i;

        post = bddmgr->ReadMemoryInUse();
        poststates = reach.CountMinterm(v->count());
    }

    pre = bddmgr->ReadMemoryInUse();
    post = bddmgr->ReadMemoryInUse();
    cout << pre << "," << post << "," << (post - pre) << endl;
    cout << prestates << "," << poststates << "," << (poststates - prestates)
            << endl;

    // When we reach here
    // We either reched a fix point of the state space
    // Or Disproved all of the formulae

    if (bmc_false_formulae->size())
    {
        cout
                << "The following formulae have been verified using BMC on the negation:"
                << endl;
        int test = 0;
        for (modal_formula_p_pair_vector::iterator iter =
                bmc_false_formulae->begin(); iter != bmc_false_formulae->end(); ++iter)
        {
            modal_formula_p_pair temp = (modal_formula_p_pair) (*iter);
            modal_formula actl = *temp.first;

            cout << "  Formula " << actl.to_string()
                    << " is FALSE in the model" << endl;
            //            no_kbar = true;
            //            build_cex(&actl, test);
            ////            //check_formulae();
            ////            no_kbar = false;
            ++test;
        }
    }

    if (!bmc_formulae->empty()) // If we have remaining unchecked formulae
    {
        is_formulae->clear(); // Remove all the old formulae

        for (modal_formula_p_pair_vector::iterator iter = bmc_formulae->begin(); iter
                != bmc_formulae->end(); ++iter)
        {
            modal_formula_p_pair temp = (modal_formula_p_pair) (*iter);
            modal_formula actl = *temp.first;
            is_formulae->push_back(actl);
            //            no_kbar = true;
            //
            //            build_cex(&actl, 0);
            //            //check_formulae();
            //            no_kbar = false;
        }

        // Use the regular check_formulae method
        check_formulae();

    }

    if (options["verbosity"] > 3)
    {
        cout << "Done" << endl;
    }
    cout << "</E4>" << endl;
}

void build_cex(modal_formula *f, int i = 0)
{
    BDD result;
    result = f->check_formula();
    //cout << "asdasd" << endl;

    countex = new vector<vector<int> *> ;
    idbdd = new map<int, BDD *> ;
    cextr = new vector<vector<transition *> *> ;

    // function to build a CEX
    if ((options["cex"] == 1))
    {

        // Computing counterexample / witness

        BDD * is = new BDD(in_st);

        countex->clear();
        idbdd->clear();
        scount = 0;
        cextr->clear();

        modal_formula * g = f->push_negations(0);

        cout << g->to_string() << endl;

        cextr->clear();

        if ((result == reach) && !(g->is_NoCTL()) && (g->is_ECTLK_new()))
        {

            // True and ECTLK: can print witness

            bool done = false;

            if (options["quiet"] == 0)
                cout << "  The following is a witness for the formula: "
                        << endl;

            while ((*is) != bddmgr->bddZero())
            {

                BDD curinitstate = is->PickOneMinterm(*v);

                if (options["debug"] == 1)
                {
                    cout << "DEBUG Computing witness with init. state : "
                            << endl;
                    cout << " ------------------------------" << endl;
                    print_state(curinitstate, *v);
                    cout << " ------------------------------" << endl;
                    cout << "DEBUG end" << endl;
                }

                if (is_valid_state(curinitstate, *v))
                {
                    //idbdd->insert(pair<int, BDD*>(0,new BDD(curinitstate)));
                    if (options["debug"] == 1)
                    {
                        cout << "DEBUG Computing witness for formula: " << endl
                                << g->to_string() << endl;
                        cout << "DEBUG end" << endl;
                    }
                    bool cexresult =
                            (is_fairness->size() > 0) ? g->build_cex_fair(
                                    &curinitstate, 0, fair_reach)
                                    : g->build_cex(&curinitstate, 0);
                    if (cexresult)
                    {
                        done = true;
                        break;
                    }
                    else
                    {
                        *is = *is - curinitstate;
                        idbdd->clear();
                        countex->clear();
                        cextr->clear();
                        scount = 0;
                    }
                }
            }

            if (!done)
            {
                if (options["quiet"] == 0)
                {
                    cout
                            << " Uhm there is a problem here: I could not compute a witness."
                            << endl;
                    cout << " Please report this problem to the authors."
                            << endl;
                }
            }
            else
            {
                if (options["quiet"] == 0)
                {

                    cout << " Witness: " << endl;
                    for (int ac = 0; ac < (int) countex->size(); ac++)
                    {
                        cout << "   < ";
                        for (int j = 0; j < (int) countex->at(ac)->size(); j++)
                        {
                            cout << countex->at(ac)->at(j) << " ";
                        }
                        cout << "> " << endl;
                    }

                    cout << "  States description: " << endl;
                    for (map<int, BDD *>::iterator iter = idbdd->begin(); iter
                            != idbdd->end(); iter++)
                    {

                        cout << "------------- State: " << (*iter).first
                                << " -----------------" << endl;
                        print_state(*(iter->second), *v);
                        cout << "----------------------------------------"
                                << endl;
                    }
                }
                else
                {
                    // Writing full witness/counterexample to text file

                    ostringstream s, s2;
                    s << "formula" << (i + 1) << ".dot";
                    s2 << "formula" << (i + 1) << ".info";
                    string filename = cex_prefix + s.str();
                    string filename2 = cex_prefix + s2.str();
                    ofstream myfile(filename.c_str());
                    ofstream myfile2(filename2.c_str());

                    if (myfile.is_open() && myfile2.is_open())
                    {
                        myfile << "digraph witness" << i << " {\n";

                        // print states and their description
                        for (map<int, BDD *>::iterator iter = idbdd->begin(); iter
                                != idbdd->end(); iter++)
                        {
                            myfile << " " << (*iter).first << " [label=\""
                                    << (*iter).first << "\",shape=ellipse]"
                                    << endl;
                            myfile2 << "-- State " << (*iter).first << " --"
                                    << endl;
                            myfile2 << state_to_str(*(iter->second), *v)
                                    << endl;
                        }

                        // printing transitions
                        // HERE
                        for (int ac = 0; ac < (int) cextr->size(); ac++)
                        {
                            for (int j = 0; j < (int) cextr->at(ac)->size(); j++)
                            {
                                cextr->at(ac)->at(j)->to_str(&myfile);
                            }
                        }

                        myfile << "}\n";

                        myfile.close();
                        myfile2.close();
                    }
                    else
                        cout << "Unable to open file";

                }
            }

        }
        else if ((result != reach) && (g->is_ACTLK_new()))
        {

            // False and ACTLK: can print counterexample

            cout << g->to_string() << endl;

            if (options["quiet"] == 0)
                cout << "  The following is a counterexampe for the formula "
                        << endl;
            bool done = false;

            // Negation of the formula:
            modal_formula * fcex = new modal_formula(3, g);
            fcex = fcex->push_negations(0);

            //cout << fcex->to_string() << endl;


            while ((*is) != bddmgr->bddZero())
            {

                BDD curinitstate = is->PickOneMinterm(*v);

                if (options["debug"] == 1)
                {
                    cout
                            << "DEBUG Computing counterexample with init. state : "
                            << endl;
                    cout << " ------------------------------" << endl;
                    print_state(curinitstate, *v);
                    cout << " ------------------------------" << endl;
                    cout << "DEBUG end" << endl;
                }

                if (is_valid_state(curinitstate, *v))
                {
                    //idbdd->insert(pair<int, BDD*>(0,new BDD(curinitstate)));


                    if (options["debug"] == 1)
                    {
                        cout << "DEBUG Computing counterexample for formula: "
                                << endl << fcex->to_string() << endl;
                        cout << "DEBUG end" << endl;
                    }
                    bool cexresult =
                            (is_fairness->size() > 0) ? fcex->build_cex_fair(
                                    &curinitstate, 0, fair_reach)
                                    : fcex->build_cex(&curinitstate, 0);
                    if (cexresult)
                    {
                        done = true;
                        break;
                    }
                    else
                    {
                        *is = *is - curinitstate;
                        idbdd->clear();
                        countex->clear();
                        cextr->clear();
                        scount = 0;
                    }
                }
            }

            if (!done)
            {
                if (options["quiet"] == 0)
                {
                    cout
                            << " Uhm there is a problem here: I could not compute a counterexample."
                            << endl;
                    cout << " Please report this problem to the authors."
                            << endl;
                }
            }
            else
            {

                if (options["quiet"] == 0)
                {
                    cout << " Counterexample: " << endl;
                    for (int ac = 0; ac < (int) countex->size(); ac++)
                    {
                        cout << "   < ";
                        for (int j = 0; j < (int) countex->at(ac)->size(); j++)
                        {
                            cout << countex->at(ac)->at(j) << " ";
                        }
                        cout << "> " << endl;
                    }

                    cout << "  States description: " << endl;
                    for (map<int, BDD *>::iterator iter = idbdd->begin(); iter
                            != idbdd->end(); iter++)
                    {

                        cout << "------------- State: " << (*iter).first
                                << " -----------------" << endl;
                        print_state(*(iter->second), *v);
                        cout << "----------------------------------------"
                                << endl;
                    }

                }
                else
                {

                    // Writing full witness/counterexample to text file

                    ostringstream s, s2;
                    s << "formula" << (i + 1) << ".dot";
                    s2 << "formula" << (i + 1) << ".info";
                    string filename = cex_prefix + s.str();
                    string filename2 = cex_prefix + s2.str();
                    ofstream myfile(filename.c_str());
                    ofstream myfile2(filename2.c_str());

                    if (myfile.is_open() && myfile2.is_open())
                    {
                        myfile << "digraph witness" << i << " {\n";

                        // print states and their description
                        for (map<int, BDD *>::iterator iter = idbdd->begin(); iter
                                != idbdd->end(); iter++)
                        {
                            myfile << " " << (*iter).first << " [label=\""
                                    << (*iter).first << "\",shape=ellipse]"
                                    << endl;
                            myfile2 << "-- State " << (*iter).first << " --"
                                    << endl;
                            myfile2 << state_to_str(*(iter->second), *v)
                                    << endl;
                        }

                        // printing transitions
                        // HERE
                        for (int ac = 0; ac < (int) cextr->size(); ac++)
                        {
                            for (int j = 0; j < (int) cextr->at(ac)->size(); j++)
                            {
                                cextr->at(ac)->at(j)->to_str(&myfile);
                            }
                        }

                        myfile << "}\n";

                        myfile.close();
                        myfile2.close();
                    }
                    else
                        cout << "Unable to open file";

                }
            }
        }
        else if (result == reach)
        {
            if (options["quiet"] == 0)
                cout
                        << "    -- Sorry it is not possible to compute witnesses for non-ECTLK formulae"
                        << endl;
        }
        else if (result != reach)
        {
            if (options["quiet"] == 0)
                cout
                        << "    -- Sorry it is not possible to compute counterexamples for non-ACTLK formulae"
                        << endl;
        }
    }
}

void check_formulae_BMC(void)
{
    string str = "_init";
    (*is_evaluation)[str] = is_istates;

    modal_formula *init = new modal_formula(new atomic_proposition(&str));

    BDD result;
    result = init->check_formula();
    if (result == in_st)
    {
        cout << "Init as expected" << endl;
    }

    double reachst = reach.CountMinterm(v->count());
    double resst = result.CountMinterm(v->count());
    cout << reachst << " , " << resst << endl;

    //cout << "BDDCACHE : " << options["bddcache"] << endl;

    for (modal_formula_p_pair_vector::iterator iter = bmc_formulae->begin(); iter
            != bmc_formulae->end();)
    {

        modal_formula_p_pair temp = (modal_formula_p_pair) (*iter);
        modal_formula * f = new modal_formula(4, init, temp.second);

        cout << temp.second->to_string() << endl;
        cout << f->to_string() << endl;

        result = f->check_formula();
        double reachst = reach.CountMinterm(v->count());
        double resst = result.CountMinterm(v->count());
        cout << reachst << " , " << resst << endl;
        //exit(-1);

        if (f)
            delete f;

        if (result == reach)
        {
            cout << "Formula is true" << endl;
            //exit(-1);
            if (options["experiment"] == 2)
            {
                cout << (temp.first)->to_string() << " FALSE " << endl;
            }
            bmc_false_formulae->push_back(temp);
            iter = bmc_formulae->erase(iter);
            //++iter;
            continue;
        }
        else if (options["experiment"] == 2)
        {
            cout << (temp.first)->to_string() << " TRUE " << endl;
        }

        ++iter;

    }
    if (init)
        delete init;
}

void check_formulae(void)
{
    need_epistemic = false;
    need_deontic = false;
    need_common_knowledge = false;
    need_deontic_knowledge = false;
    need_distributed_knowledge = false;

    for (vector<modal_formula>::iterator i = is_formulae->begin(); i
            != is_formulae->end(); i++)
        i->look_flags(&need_epistemic, &need_deontic, &need_common_knowledge,
                &need_deontic_knowledge, &need_distributed_knowledge);

    if (need_epistemic)
    {
        //obsvars_bdd_length = (*agents)[0]->obsvars_BDD_length();
        if (options["quiet"] == 0 || options["simulation"] == 0)
            cout << "Building OBDD for epistemic relations..." << endl;

        //BDD epistemic;// = bddmgr->bddOne();
        int length = 0; //is_environment->state_BDD_length();
        int position = 0;
        //for(int i=position; i<position+length; i++)
        //  epistemic = epistemic * ( ( !v[i] + pv[i] ) *
        //			( v[i] + !pv[i] ) );
        //pair<string, BDD> p("Environment", epistemic);
        //er.insert(p);
        //position += length;
        //    epistemic.print(2,2);
        for (unsigned int k = 0; k < agents->size(); k++)
        {
            BDD epistemic = bddmgr->bddOne();
            length = (*agents)[k]->state_BDD_length();
            for (int i = position; i < position + length; i++)
                epistemic = epistemic * ((!(*v)[i] + (*pv)[i]) * ((*v)[i]
                        + !(*pv)[i]));
            if (k > 0)
            {
                // global observale variables
                for (int i = 0; i < obsvars_bdd_length; i++)
                    epistemic = epistemic * ((!(*v)[i] + (*pv)[i]) * ((*v)[i]
                            + !(*pv)[i]));
                // local observable variables
                map<string, variable*>* lobsvars = (*agents)[k]->get_lobsvars();
                if (lobsvars != NULL && lobsvars->size() > 0)
                    for (map<string, variable *>::iterator x =
                            lobsvars->begin(); x != lobsvars->end(); x++)
                    {
                        basictype* bt = x->second->get_var_type();
                        unsigned char bt_type = bt->get_type();
                        int index_begin, index_end;
                        if (bt_type == 1)
                        {// boolean
                            index_begin = bt->get_index_begin();
                            index_end = bt->get_index_begin();
                        }
                        else if (bt_type == 2)
                        {// boolean
                            index_begin = ((rangedint*) bt)->get_index_begin();
                            index_end = ((rangedint*) bt)->get_index_begin();
                        }
                        else
                        {
                            index_begin = ((enumerate*) bt)->get_index_begin();
                            index_end = ((enumerate*) bt)->get_index_begin();
                        }
                        for (int i = index_begin; i <= index_end; i++)
                            epistemic = epistemic * ((!(*v)[i] + (*pv)[i])
                                    * ((*v)[i] + !(*pv)[i]));
                    }
            }
            er.insert(pair<string, BDD> ((*agents)[k]->get_name(), epistemic));
            position += length;
        }

        if (options["verbosity"] > 4)
            cout << "Done." << endl;
    }

    if (need_deontic)
    {
        if (options["quiet"] == 0 || options["simulation"] == 0)
            cout << "Building OBDD for deontic relations..." << endl;
        //BDD deontic; // = is_environment->encode_greenstates(pv, a, bddmgr);
        //pair<string, BDD> p("Environment", deontic);
        //deor.insert(p);
        for (unsigned int k = 0; k < agents->size(); k++)
        {
            BDD deontic = (*agents)[k]->encode_greenstates();
            deor.insert(pair<string, BDD> ((*agents)[k]->get_name(), deontic));
        }

        if (options["verbosity"] > 4)
        {
            cout << "Done." << endl;
        }
    }

    // Building group modalities
    if (is_groups != NULL && is_groups->size() > 0)
    {
        if (options["quiet"] == 0 || options["simulation"] == 0)
        {
            cout << "Building OBDD for group modalities..." << endl;
        }

        BDD egm; // Epistemic group modality
        BDD dgm; // Deontic group modality
        BDD tmpdistgm; // Distributed knowledge
        set<string> names_g;
        BDD swapreach = reach.SwapVariables(*v, *pv);

        if (need_common_knowledge && options["lazyGCK"] == 0)
        {
            if (options["verbosity"] > 4)
                cout << "    Building OBDD for everybody knows...";

            for (map<string, set<string> >::iterator gi = is_groups->begin(); gi
                    != is_groups->end(); gi++)
            {
                // Epistemic first
                egm = bddmgr->bddZero();
                names_g = gi->second;
                //for (set<string>::iterator igs=names_g.begin(); igs!=names_g.end(); igs++)
                //egm = (egm + er[*igs])*reach*swapreach;
                for (set<string>::iterator igs = names_g.begin(); igs
                        != names_g.end(); igs++)
                    egm += er[*igs];
                egm *= reach * swapreach;

                /*BDD testegm = bddmgr->bddZero();
                 for (set<string>::iterator igs=names_g.begin(); igs!=names_g.end(); igs++)
                 testegm += er[*igs]*reach*swapreach;
                 if(egm != testegm)
                 cout << "new way is not correct" << endl;
                 else
                 cout << "new way is correct" << endl;*/

                gm[gi->first] = egm;
                //egm.print(2,2);
            }

            if (options["verbosity"] > 4)
                cout << "Done." << endl;
        }

        if (need_deontic_knowledge)
        {
            if (options["verbosity"] > 4)
                cout << "    Building OBDD for deontic knowledge...";

            for (map<string, set<string> >::iterator gi = is_groups->begin(); gi
                    != is_groups->end(); gi++)
            {
                // Deontic
                dgm = bddmgr->bddOne();
                names_g = gi->second;
                for (set<string>::iterator igs = names_g.begin(); igs
                        != names_g.end(); igs++)
                    dgm = (dgm * deor[*igs]) * reach * swapreach;

                /** Can it be the following code
                 for (set<string>::iterator igs=names_g.begin(); igs!=names_g.end(); igs++)
                 dgm *= deor[*igs];
                 dgm *= reach*swapreach;
                 */

                deogm[gi->first] = dgm;
            }

            if (options["verbosity"] > 4)
                cout << "Done." << endl;
        }

        if (need_distributed_knowledge)
        {
            if (options["verbosity"] > 4)
                cout << "    Building OBDD for distributed knowledge...";

            for (map<string, set<string> >::iterator gi = is_groups->begin(); gi
                    != is_groups->end(); gi++)
            {
                // Deontic
                tmpdistgm = bddmgr->bddOne();
                names_g = gi->second;
                for (set<string>::iterator igs = names_g.begin(); igs
                        != names_g.end(); igs++)
                    tmpdistgm = (tmpdistgm * er[*igs]) * reach * swapreach;

                /** Can it be the following code
                 for (set<string>::iterator igs=names_g.begin(); igs!=names_g.end(); igs++)
                 tmpdistgm *= er[*igs];
                 tmpdistgm *= reach*swapreach;
                 */

                distgm[gi->first] = tmpdistgm;
            }
            if (options["verbosity"] > 4)
                cout << "Done." << endl;
        }

        if (options["verbosity"] > 4)
            cout << "  Done: group modalities encoded successfully" << endl;
    }
    //MCMAS_Cudd_AutodynEnable(bddmgr->getManager(), CUDD_REORDER_SIFT);

    if (options["quiet"] == 0)
        cout << "Done." << endl;

    if (options["quiet"] == 0)
        cout << "Checking formulae..." << endl;

    string str = "_init";
    (*is_evaluation)[str] = is_istates;
    modal_formula *init = new modal_formula(new atomic_proposition(&str));

    if (is_fairness->size() > 0)
    {
        if (options["quiet"] == 0 || options["simulation"] == 0)
            cout << "Building set of fair states..." << endl;

        if ((options["bddcache"] == 2 || options["bddcache"] == 3)
                && symmetry_cache == NULL)
        {
            symmetry_cache = new map<string, BDD> ();
            (*symmetry_cache)["_init"] = in_st;
        }

        modal_formula *neg_init = new modal_formula(3, init);

        modal_formula *taut = new modal_formula(2, init, neg_init);

        for (vector<fairness_expression *>::iterator i = is_fairness->begin(); i
                != is_fairness->end(); i++)
        {
            BDD fairset = (*i)->check_formula();
            (*i)->set_bdd_representation(fairset);
        }

        modal_formula *eg_true = new modal_formula(11, taut); // This is EG(True)

        // This is a set of "fair" states (the beginning of a fair computation)
        fair_reach = eg_true->check_formula_fair(bddmgr->bddOne());

        if (options["debug"] == 1)
        {
            cout
                    << "DEBUG: the set of fair states (beginning of a fair computation)"
                    << endl;
            fair_reach.print(v->count(), 2);
            cout << "DEBUG end" << endl;
        }
    } // end if

    countex = new vector<vector<int> *> ;
    idbdd = new map<int, BDD *> ;
    cextr = new vector<vector<transition *> *> ;

    if (options["quiet"] == 0 || options["simulation"] == 0)
        cout << "Verifying properties..." << endl;

    BDD result;
    if (options["globalcheck"] == 1)
    { // Check formula on all states
        for (unsigned int i = 0; i < is_formulae->size(); i++)
        {
            result
                    = is_fairness->size() > 0 ? (*is_formulae)[i].check_formula_fair(
                            fair_reach)
                            : (*is_formulae)[i].check_formula();
            if (options["quiet"] == 0)
                cout << "  Formula number " << i << ": "
                        << (*is_formulae)[i].to_string() << ", is " << (result
                        == reach ? "TRUE" : "FALSE") << " in the model" << endl;
            else
                cout << (result == reach ? "TRUE" : "FALSE") << endl;
        }
    }
    if (options["symmetry"] > 0)
    { // Check formula by symmetry reduction
        symmetry_cache = new map<string, BDD> ();
        symmetry_atom_cache = new map<string, string> ();
        set<string>* formulas;
        for (map<string, bool_expression*>::iterator i = is_evaluation->begin(); i
                != is_evaluation->end(); i++)
            if ((i->first).find(".") == string::npos)
            {
                if ((i->first).compare("_init") != 0)
                {
                    //cout << "encoding " << i->first << endl;
                    BDD tmp = i->second->encode_bdd(bddOne) * reach;
                    (*symmetry_cache)[i->first] = tmp;
                    (*symmetry_atom_cache)[i->second->to_string()] = i->first;
                }
                else
                {
                    (*symmetry_cache)[i->first] = in_st;
                }
            }
        vector<map<string, string>*>* permutations = (options["symmetry"] % 2)
                == 1 ? compute_round_permutation()
                : compute_arbitrary_permutation();
        for (unsigned int i = 0; i < is_formulae->size(); i++)
        {
            bool flag = true;
            if ((options["symmetry"] % 2) == 0)
                formulas = new set<string> ;
            for (unsigned int j = 0; j < permutations->size(); j++)
            {
                modal_formula *newformula = ((*is_formulae)[i]).permute_agents(
                        (*permutations)[j]);
                string fstr = newformula->to_string();
                if ((options["symmetry"] % 2) == 0)
                {
                    if (formulas->find(fstr) != formulas->end())
                    {
                        //cout << "formula found:" << fstr << endl;
                        continue;
                    }
                    else
                        formulas->insert(fstr);
                }
                modal_formula * f = new modal_formula(4, init, newformula);
                result = f->check_formula_symmetry(permutations);
                if (result != reach)
                {
                    flag = false;
                    break;
                }
            }
            cout << (flag ? "TRUE" : "FALSE") << endl;
        }
    }
    else
    {
        if ((options["bddcache"] == 2 || options["bddcache"] == 3)
                && symmetry_cache == NULL)
        {
            symmetry_cache = new map<string, BDD> ();
            (*symmetry_cache)["_init"] = in_st;
        }

        //        unsigned int success_count = 0;
        //        bmc_succeeded = false;
        for (unsigned int i = 0; i < is_formulae->size(); i++)
        {
            scount = 0;
            modal_formula * f =
                    new modal_formula(4, init, &((*is_formulae)[i]));
            result
                    = is_fairness->size() > 0 ? f->check_formula_fair(
                            fair_reach) : f->check_formula();

            //            success_count += ((result == reach) ? 1 : 0);

            if (options["debug"] == 1)
            {
                cout << "DEBUG RESULT: " << endl;
                //result.print(2,2);
                cout << "REACH" << endl;
                reach.print(2, 2);
                cout << "DEBUG end" << endl;
            }

            if (options["quiet"] == 0)
                cout << "  Formula " << (*is_formulae)[i].to_string() << " is "
                        << (result == reach ? "TRUE" : "FALSE")
                        << " in the model" << endl;
            else
                cout << (result == reach ? "TRUE" : "FALSE") << endl;

            no_kbar = true;
            if ((options["cex"] == 1))
            {

                // Computing counterexample / witness

                BDD * is = new BDD(in_st);

                countex->clear();
                idbdd->clear();
                scount = 0;
                cextr->clear();

                modal_formula * g = f->push_negations(0);

                cextr->clear();

                if ((result == reach) && !(g->is_NoCTL())
                        && (g->is_ECTLK_new()))
                {

                    // True and ECTLK: can print witness

                    bool done = false;

                    if (options["quiet"] == 0)
                        cout
                                << "  The following is a witness for the formula: "
                                << endl;

                    while ((*is) != bddmgr->bddZero())
                    {

                        BDD curinitstate = is->PickOneMinterm(*v);

                        if (options["debug"] == 1)
                        {
                            cout
                                    << "DEBUG Computing witness with init. state : "
                                    << endl;
                            cout << " ------------------------------" << endl;
                            print_state(curinitstate, *v);
                            cout << " ------------------------------" << endl;
                            cout << "DEBUG end" << endl;
                        }

                        if (is_valid_state(curinitstate, *v))
                        {
                            //idbdd->insert(pair<int, BDD*>(0,new BDD(curinitstate)));
                            if (options["debug"] == 1)
                            {
                                cout << "DEBUG Computing witness for formula: "
                                        << endl << g->to_string() << endl;
                                cout << "DEBUG end" << endl;
                            }
                            bool
                                    cexresult =
                                            (is_fairness->size() > 0) ? g->build_cex_fair(
                                                    &curinitstate, 0,
                                                    fair_reach)
                                                    : g->build_cex(
                                                            &curinitstate, 0);
                            if (cexresult)
                            {
                                done = true;
                                break;
                            }
                            else
                            {
                                *is = *is - curinitstate;
                                idbdd->clear();
                                countex->clear();
                                cextr->clear();
                                scount = 0;
                            }
                        }
                    }

                    if (!done)
                    {
                        if (options["quiet"] == 0)
                        {
                            cout
                                    << " Uhm there is a problem here: I could not compute a witness."
                                    << endl;
                            cout
                                    << " Please report this problem to the authors."
                                    << endl;
                        }
                    }
                    else
                    {
                        if (options["quiet"] == 0)
                        {

                            cout << " Witness: " << endl;
                            for (int ac = 0; ac < (int) countex->size(); ac++)
                            {
                                cout << "   < ";
                                for (int j = 0; j
                                        < (int) countex->at(ac)->size(); j++)
                                {
                                    cout << countex->at(ac)->at(j) << " ";
                                }
                                cout << "> " << endl;
                            }

                            cout << "  States description: " << endl;
                            for (map<int, BDD *>::iterator iter =
                                    idbdd->begin(); iter != idbdd->end(); iter++)
                            {

                                cout << "------------- State: "
                                        << (*iter).first
                                        << " -----------------" << endl;
                                print_state(*(iter->second), *v);
                                cout
                                        << "----------------------------------------"
                                        << endl;
                            }
                        }
                        else
                        {
                            // Writing full witness/counterexample to text file

                            ostringstream s, s2;
                            s << "formula" << (i + 1) << ".dot";
                            s2 << "formula" << (i + 1) << ".info";
                            string filename = cex_prefix + s.str();
                            string filename2 = cex_prefix + s2.str();
                            ofstream myfile(filename.c_str());
                            ofstream myfile2(filename2.c_str());

                            if (myfile.is_open() && myfile2.is_open())
                            {
                                myfile << "digraph witness" << i << " {\n";

                                // print states and their description
                                for (map<int, BDD *>::iterator iter =
                                        idbdd->begin(); iter != idbdd->end(); iter++)
                                {
                                    myfile << " " << (*iter).first
                                            << " [label=\"" << (*iter).first
                                            << "\",shape=ellipse]" << endl;
                                    myfile2 << "-- State " << (*iter).first
                                            << " --" << endl;
                                    myfile2
                                            << state_to_str(*(iter->second), *v)
                                            << endl;
                                }

                                // printing transitions
                                // HERE
                                for (int ac = 0; ac < (int) cextr->size(); ac++)
                                {
                                    for (int j = 0; j
                                            < (int) cextr->at(ac)->size(); j++)
                                    {
                                        cextr->at(ac)->at(j)->to_str(&myfile);
                                    }
                                }

                                myfile << "}\n";

                                myfile.close();
                                myfile2.close();
                            }
                            else
                                cout << "Unable to open file";

                        }
                    }

                }
                else if ((result != reach) && (g->is_ACTLK_new()))
                {

                    // False and ACTLK: can print counterexample

                    cout << g->to_string() << endl;

                    if (options["quiet"] == 0)
                        cout
                                << "  The following is a counterexampe for the formula "
                                << endl;
                    bool done = false;

                    // Negation of the formula:
                    modal_formula * fcex = new modal_formula(3, g);
                    fcex = fcex->push_negations(0);

                    cout << fcex->to_string() << endl;

                    //cout << fcex->to_string() << endl;


                    while ((*is) != bddmgr->bddZero())
                    {

                        BDD curinitstate = is->PickOneMinterm(*v);

                        if (options["debug"] == 1)
                        {
                            cout
                                    << "DEBUG Computing counterexample with init. state : "
                                    << endl;
                            cout << " ------------------------------" << endl;
                            print_state(curinitstate, *v);
                            cout << " ------------------------------" << endl;
                            cout << "DEBUG end" << endl;
                        }

                        if (is_valid_state(curinitstate, *v))
                        {
                            //idbdd->insert(pair<int, BDD*>(0,new BDD(curinitstate)));


                            if (options["debug"] == 1)
                            {
                                cout
                                        << "DEBUG Computing counterexample for formula: "
                                        << endl << fcex->to_string() << endl;
                                cout << "DEBUG end" << endl;
                            }
                            bool
                                    cexresult =
                                            (is_fairness->size() > 0) ? fcex->build_cex_fair(
                                                    &curinitstate, 0,
                                                    fair_reach)
                                                    : fcex->build_cex(
                                                            &curinitstate, 0);
                            if (cexresult)
                            {
                                done = true;
                                break;
                            }
                            else
                            {
                                *is = *is - curinitstate;
                                idbdd->clear();
                                countex->clear();
                                cextr->clear();
                                scount = 0;
                            }
                        }
                    }

                    if (!done)
                    {
                        if (options["quiet"] == 0)
                        {
                            cout
                                    << " Uhm there is a problem here: I could not compute a counterexample."
                                    << endl;
                            cout
                                    << " Please report this problem to the authors."
                                    << endl;
                        }
                    }
                    else
                    {

                        if (options["quiet"] == 0)
                        {
                            cout << " Counterexample: " << endl;
                            for (int ac = 0; ac < (int) countex->size(); ac++)
                            {
                                cout << "   < ";
                                for (int j = 0; j
                                        < (int) countex->at(ac)->size(); j++)
                                {
                                    cout << countex->at(ac)->at(j) << " ";
                                }
                                cout << "> " << endl;
                            }

                            cout << "  States description: " << endl;
                            for (map<int, BDD *>::iterator iter =
                                    idbdd->begin(); iter != idbdd->end(); iter++)
                            {

                                cout << "------------- State: "
                                        << (*iter).first
                                        << " -----------------" << endl;
                                print_state(*(iter->second), *v);
                                cout
                                        << "----------------------------------------"
                                        << endl;
                            }

                        }
                        else
                        {

                            // Writing full witness/counterexample to text file

                            ostringstream s, s2;
                            s << "formula" << (i + 1) << ".dot";
                            s2 << "formula" << (i + 1) << ".info";
                            string filename = cex_prefix + s.str();
                            string filename2 = cex_prefix + s2.str();
                            ofstream myfile(filename.c_str());
                            ofstream myfile2(filename2.c_str());

                            if (myfile.is_open() && myfile2.is_open())
                            {
                                myfile << "digraph witness" << i << " {\n";

                                // print states and their description
                                for (map<int, BDD *>::iterator iter =
                                        idbdd->begin(); iter != idbdd->end(); iter++)
                                {
                                    myfile << " " << (*iter).first
                                            << " [label=\"" << (*iter).first
                                            << "\",shape=ellipse]" << endl;
                                    myfile2 << "-- State " << (*iter).first
                                            << " --" << endl;
                                    myfile2
                                            << state_to_str(*(iter->second), *v)
                                            << endl;
                                }

                                // printing transitions
                                // HERE
                                for (int ac = 0; ac < (int) cextr->size(); ac++)
                                {
                                    for (int j = 0; j
                                            < (int) cextr->at(ac)->size(); j++)
                                    {
                                        cextr->at(ac)->at(j)->to_str(&myfile);
                                    }
                                }

                                myfile << "}\n";

                                myfile.close();
                                myfile2.close();
                            }
                            else
                                cout << "Unable to open file";

                        }
                    }
                }
                else if (result == reach)
                {
                    if (options["quiet"] == 0)
                        cout
                                << "    -- Sorry it is not possible to compute witnesses for non-ECTLK formulae"
                                << endl;
                }
                else if (result != reach)
                {
                    if (options["quiet"] == 0)
                        cout
                                << "    -- Sorry it is not possible to compute counterexamples for non-ACTLK formulae"
                                << endl;
                }
            }
            no_kbar = false;
            if ((options["cex"] == 1) && (result != reach))
            {
                BDD c = reach * (!result);

                if (!(is_fairness->size() > 0))
                {
                    fair_reach = reach;
                }

                //f.build_cex();
            }

        }
        //        bmc_succeeded = (success_count == is_formulae->size());
    }

}

void print_help(void)
{
    cout << "Usage: " << NAME << " [OPTIONS] FILE " << endl;
    cout << "Example: " << NAME << " -v 3 -bdd_stats myfile.ispl" << endl;
    cout << endl << "Options: " << endl;
    cout << "  -s \t \t Interactive execution" << endl;
    cout << "  -v Number \t verbosity level ( 0 -- 5, default 0 )" << endl;
    cout
            << "  -e Number \t Choose the approach to do model checking (0 -- 3, default 1)"
            << endl;
    //cout << "  -bc Number \t Store some BDDs to speed up verification (1: RT*reach only, 2: atomic propositions only, 3: both (default))" << endl;
    cout
            << "  -fe Number \t A new way to encode evolution functions and initial states (1: evolution only, 2: initial state only, 3: both)"
            << endl;
    cout << "  -if \t \t Encode initial states first" << endl;
    cout << "  -bdd_stats \t Print BDD statistics " << endl;
    //cout << "  -lgck \t \t lazy instantiation of group modality " << endl;
    //cout << "  -src \t \t Print parsed ISPL source code and exit" << endl;
    //cout << "  -gsc \t \t Check the syntax and exit " << endl;
    cout << "  -c \t \t Print counterexamples or witness executions" << endl;
    //cout << "  -cex_prefix \t Destination directory for counterexample files" << endl;
    cout
            << "  -g \t \t Check formulas globally (i.e., not only on initial states)"
            << endl;
    //cout << "  -d \t \t Run in debug mode" << endl;
    cout << "  -h \t \t This screen" << endl;
    cout << endl
            << "Report bugs to <hongyang.qu@imperial.ac.uk> or <f.raimondi@cs.ucl.ac.uk>"
            << endl;

}

void print_banner(void)
{
    cout
            << "********************************************************************************"
            << endl;
    cout << "                       MCMAS v0.9.7 " << endl << endl;
    cout << " This software comes with ABSOLUTELY NO WARRANTY, to the extent"
            << endl;
    cout << " permitted by applicable law. " << endl << endl;
    cout << " Please check " << endl << " " << URL << endl;
    cout
            << " for the latest release.\n Report bugs to <hongyang.qu@imperial.ac.uk> or <f.raimondi@cs.ucl.ac.uk>"
            << endl;
    cout
            << "********************************************************************************"
            << endl << endl;
}

void print_ispl_code(void)
{
    for (unsigned int i = 0; i < agents->size(); i++)
        cout << (*agents)[i]->to_string() << endl;
    cout << "Evaluation" << endl;
    for (map<string, bool_expression *>::iterator i = is_evaluation->begin(); i
            != is_evaluation->end(); i++)
        cout << "    " << (*i).first << " if " << (*i).second->to_string()
                << ";" << endl;
    cout << "end Evaluation" << endl << endl;
    cout << "InitStates" << endl << "    " << is_istates->to_string() << ";"
            << endl << "end InitStates" << endl << endl;
    cout << "Group" << endl;
    for (map<string, set<string> >::iterator i = is_groups->begin(); i
            != is_groups->end(); i++)
    {
        cout << "    " << (*i).first << " = { ";
        int k = 0;
        int bound = ((*i).second).size() - 1;
        for (set<string>::iterator j = ((*i).second).begin(); j
                != ((*i).second).end(); j++)
        {
            if (k == bound)
                cout << (*j) << " ";
            else
                cout << (*j) << ", ";
            k++;
        }
        cout << "}; " << endl;
    }
    cout << "end Group" << endl << endl;
    cout << "Fairness" << endl;
    for (vector<fairness_expression*>::iterator i = is_fairness->begin(); i
            != is_fairness->end(); i++)
        cout << "    " << (*i)->to_string() << ";" << endl;
    cout << "end Fairness" << endl << endl;
    cout << "Formulae" << endl;
    for (vector<modal_formula>::iterator i = is_formulae->begin(); i
            != is_formulae->end(); i++)
        cout << "    " << (*i).to_string() << ";" << endl;
    cout << "end Formulae" << endl;
}

void print_state(BDD state, BDDvector v)
{
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        cout << "Agent " << (*agents)[i]->get_name() << endl;
        (*agents)[i]->print_state("  ", state, v);
    }
}

string state_to_str(BDD state, BDDvector v)
{
    ostringstream s;

    for (unsigned int i = 0; i < agents->size(); i++)
    {
        s << "  Agent " << (*agents)[i]->get_name() << "\n";
        s << (*agents)[i]->state_to_str(state, v);

    }
    return s.str();
}

bool find_same_state(map<string, int> *statehash, string state)
{
    if (statehash != NULL)
    {
        map<string, int>::iterator iter = statehash->find(state);
        if (iter != statehash->end())
        {
            //cout << "find a redundant state" << endl;
            return true;
        }
    }
    return false;
}

bool is_valid_state(BDD state, BDDvector v)
{
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        if (!(*agents)[i]->is_valid_state(state, v))
            return false;
    }
    return true;
}

void print_action(BDD state, BDDvector a)
{
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        cout << (*agents)[i]->get_name() << " : ";
        (*agents)[i]->print_action(state, a);
        if (i < agents->size() - 1)
            cout << "; ";
        else
            cout << endl;
    }
}

void print_action_1(BDD state, BDDvector a)
{
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        cout << (*agents)[i]->get_name() << " : ";
        (*agents)[i]->print_action(state, a);
        cout << "; ";
    }
    cout << endl;
}

bool is_valid_action(BDD state, BDDvector a)
{
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        if (!(*agents)[i]->is_valid_action(state, a))
            return false;
    }
    return true;
}

BDD append_variable_BDDs(BDD a)
{
    for (unsigned int j = 0; j < agents->size(); j++)
    {
        map<string, basictype *> *obsvars = (*agents)[j]->get_obsvars();
        if (obsvars != NULL && obsvars->size() > 0)
            for (map<string, basictype *>::iterator i = obsvars->begin(); i
                    != obsvars->end(); i++)
                if ((*i).second->get_type() == 3)
                    a *= ((enumerate *) (*i).second)->build_all_BDDs();
        map<string, basictype *> *vars = (*agents)[j]->get_vars();
        if (vars != NULL && vars->size() > 0)
            for (map<string, basictype *>::iterator i = vars->begin(); i
                    != vars->end(); i++)
                if ((*i).second->get_type() == 3)
                    a *= ((enumerate *) (*i).second)->build_all_BDDs();
    }
    return a;
}
